Library ▹ Essentials ▹ Sets
Proposition 1.1.22.  Let S be a set. Then:
S ∪ ∅ = S
Proof.
  • Trivial.
  • By 1.1.20.
References.
  • https://proofwiki.org/wiki/Union_with_Empty_Set
  • http://metamath.tirix.org/un0.html
  • https://leanprover-community.github.io/mathlib_docs/data/set/basic.html#set.union_empty
[View Source]