Library
▹
Essentials
▹
Sets
Proposition 1.1.23.
Let
S
be a set. Then:
∅ ∪
S
=
S
Proof.
Trivial.
By
1.1.21
.
References.
https://leanprover-community.github.io/mathlib_docs/data/set/basic.html#set.empty_union