Maths in Lean : sets

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 XX 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