Library
▹
Essentials
▹
Sets
Proposition 1.1.20.
Let
U
be a set,
S
,
T
⊆
U
. Then:
S
⊆
S
∪
T
Proof.
Let
x
∈
S
. Then
x
∈
S
∪
T
by definition.
References.
https://proofwiki.org/wiki/Set_is_Subset_of_Union
http://metamath.tirix.org/ssun1.html
https://leanprover-community.github.io/mathlib_docs/data/set/basic.html#set.subset_union_left