Section 5 : Sets

Note to future Kevin: this needs to be moved to section 4, and functions to section 3, and groups to section 5.

Lean uses type theory, not set theory. Lean has sets, but they’re always subsets of a type. For example, the real numbers ℝ are a type in Lean, so you can make sets of real numbers. The type of sets of real numbers is called set ℝ in Lean. More generally if X is any type, set X is the type of subsets of X.

Remember that in Lean’s type theory, every object lives at one of three “levels”. There are the two universes Type and Prop at the top, and then there are the types and the theorem statements one level below them, and then there are the terms and the theorem proofs at the bottom. The type of all real numbers ℝ is a type, so ℝ lives at the middle level, and real numbers like 7 are terms; we write 7 : ℝ to indicate that 7 is a real number.

Here’s how sets fit into the picture, and it might not be how you think. The type set ℝ is the type of sets of real numbers, so set ℝ : Type. A term of this type is hence a term, so at the bottom level. Let S : set ℝ be a set of real numbers. Then S is a term, not a type, so 3 : S doesn’t make sense (because t : T means that t is a term and T is a type). So how do we talk about elements of sets? The same way that mathematicians do. If x : ℝ is a real number, then we write x ∈ S to mean that x is an element of the set S. Note that both x and S in x ∈ S are terms. Note also that x ∈ S : Prop, i.e. x ∈ S is a true-false statement.

The ext tactic is a useful one to know when dealing with equalities of sets. Extensionality is a mathematical principle which states that two objects are equal if they’re made from the same things. For example, sets are extensional objects in mathematics, which means that two sets are equal if and only if they have the same elements. If S : set ℝ and T : set ℝ are sets, and your goal is ⊢ S = T then the tactic ext x will introduce a new arbitrary real number x : ℝ into the tactic state, and will turn the goal into x ∈ S ↔ x ∈ T.