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