The word set in Lean is best explained to a mathematician as meaning “subset of”. For example X : set nat means that X is a subset of the natural numbers (or “a set of naturals”). The way these are implemented is that if Y is a type, then X : set Y actually means that X is a map Y -> Prop, to be thought of as sending an object y of type Y to the Proposition “I am in X” (of course this can be true or false).
Sets are defined in init/data/set.lean in the core Lean library. Note that because of the way things are set up, if X : set Y then there is not a natural map from type X to type Y! In fact this fails for two reasons. Firstly I am not sure it even makes sense to have something of type X — X is just a function. The other issue is that Y itself does not have type set Y; the “set version” of Y is called univ : set Y and it corresponds to the function Y -> Prop sending every y : Y to true : Prop. Here are some examples of sets in action.
Examples.
variable (Y : Type*)
variables (A B : set Y)
variable (y : Y)
-- \subseteq
#check A ⊆ B
-- \in
#check y ∈ A
#check -A -- complement of A in Y
example : A ⊆ set.univ := λ y Hy, trivial -- presumably in mathlib
-- \empty
example : ∅ ⊆ A := λ y Hy, false.elim Hy -- result presumably in mathlib
-- \union
example : A ⊆ A ∪ B := λ y Hy,or.inl Hy -- result presumably in mathlib
-- \cap
example : A ∩ B ⊆ A := λ y Hy, and.elim_left Hy -- result presumably in mathlib
-- TODO : give better proofs
Xena 