Library
▹
Essentials
▹
Sets
Proposition 1.1.11.
Let
S
be a set. Then:
S
∩
S
=
S
Proof.
Trivial.
Let
x
∈
S
. Then
x
∈
S
∩
S
by definition.
References.
https://proofwiki.org/wiki/Intersection_is_Idempotent
http://metamath.tirix.org/inidm.html
https://leanprover-community.github.io/mathlib_docs/data/set/basic.html#set.inter_self