Note about Mathlib/Init/

The files in Mathlib/Init are leftovers from the port from Mathlib3. (They contain content moved from lean3 itself that Mathlib needed but was not moved to lean4.)

We intend to move all the content of these files out into the main Mathlib directory structure. Contributions assisting with this are appreciated.

Sets

This file sets up the theory of sets whose elements have a given type.

Main definitions

Given a type X and a predicate p : X → Prop:

• Set X : the type of sets whose elements have type X
• {a : X | p a} : Set X : the set of all elements of X satisfying p
• {a | p a} : Set X : a more concise notation for {a : X | p a}
• {f x y | (x : X) (y : Y)} : Set Z : a more concise notation for {z : Z | ∃ x y, f x y = z}
• {a ∈ S | p a} : Set X : given S : Set X, the subset of S consisting of its elements satisfying p.

Implementation issues

As in Lean 3, Set X := X → Prop

I didn't call this file Data.Set.Basic because it contains core Lean 3 stuff which happens before mathlib3's data.set.basic . This file is a port of the core Lean 3 file lib/lean/library/init/data/set.lean.

def Set (α : Type u) : Type u

A set is a collection of elements of some type α.

Although Set is defined as α → Prop, this is an implementation detail which should not be relied on. Instead, setOf and membership of a set (∈) should be used to convert between sets and predicates.

Equations

• Set α = (α → Prop)

def setOf {α : Type u} (p : α → Prop) : Set α

Turn a predicate p : α → Prop into a set, also written as {x | p x}

Equations

• setOf p = p

def Set.Mem {α : Type u} (a : α) (s : Set α) : Prop

Membership in a set

Equations

• Set.Mem a s = s a

instance Set.instMembership {α : Type u} : Membership α (Set α)

Equations

• Set.instMembership = { mem := Set.Mem }

theorem Set.ext {α : Type u} {a : Set α} {b : Set α} (h : ∀ (x : α), x ∈ a ↔ x ∈ b) : a = b

def Set.Subset {α : Type u} (s₁ : Set α) (s₂ : Set α) : Prop

The subset relation on sets. s ⊆ t means that all elements of s are elements of t.

Note that you should not use this definition directly, but instead write s ⊆ t.

Equations

• s₁.Subset s₂ = ∀ ⦃a : α⦄, a ∈ s₁ → a ∈ s₂

instance Set.instLE {α : Type u} : LE (Set α)

Porting note: we introduce ≤ before ⊆ to help the unifier when applying lattice theorems to subset hypotheses.

Equations

• Set.instLE = { le := Set.Subset }

instance Set.instHasSubset {α : Type u} : HasSubset (Set α)

Equations

• Set.instHasSubset = { Subset := fun (x x_1 : Set α) => x ≤ x_1 }

instance Set.instEmptyCollection {α : Type u} : EmptyCollection (Set α)

Equations

• Set.instEmptyCollection = { emptyCollection := fun (x : α) => False }

def Set.«term{_|_}» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Set.setOf.unexpander : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

def Set.«term{_|_}_1» : Lean.ParserDescr

{ f x y | (x : X) (y : Y) } is notation for the set of elements f x y constructed from the binders x and y, equivalent to {z : Z | ∃ x y, f x y = z}.

If f x y is a single identifier, it must be parenthesized to avoid ambiguity with {x | p x}; for instance, {(x) | (x : Nat) (y : Nat) (_hxy : x = y^2)}.

Equations

• One or more equations did not get rendered due to their size.

def Set.macroPattSetBuilder : Lean.ParserDescr

• { pat : X | p } is notation for pattern matching in set-builder notation, where pat is a pattern that is matched by all objects of type X and p is a proposition that can refer to variables in the pattern. It is the set of all objects of type X which, when matched with the pattern pat, make p come out true.
• { pat | p } is the same, but in the case when the type X can be inferred.

For example, { (m, n) : ℕ × ℕ | m * n = 12 } denotes the set of all ordered pairs of natural numbers whose product is 12.

Note that if the type ascription is left out and p can be interpreted as an extended binder, then the extended binder interpretation will be used. For example, { n + 1 | n < 3 } will be interpreted as { x : Nat | ∃ n < 3, n + 1 = x } rather than using pattern matching.

Equations

• One or more equations did not get rendered due to their size.

def Set.«term{_|_}_2» : Lean.ParserDescr

• { pat : X | p } is notation for pattern matching in set-builder notation, where pat is a pattern that is matched by all objects of type X and p is a proposition that can refer to variables in the pattern. It is the set of all objects of type X which, when matched with the pattern pat, make p come out true.
• { pat | p } is the same, but in the case when the type X can be inferred.

For example, { (m, n) : ℕ × ℕ | m * n = 12 } denotes the set of all ordered pairs of natural numbers whose product is 12.

Note that if the type ascription is left out and p can be interpreted as an extended binder, then the extended binder interpretation will be used. For example, { n + 1 | n < 3 } will be interpreted as { x : Nat | ∃ n < 3, n + 1 = x } rather than using pattern matching.

Equations

• One or more equations did not get rendered due to their size.

def Set.setOfPatternMatchUnexpander : Lean.PrettyPrinter.Unexpander

Pretty printing for set-builder notation with pattern matching.

Equations

• One or more equations did not get rendered due to their size.

def Set.univ {α : Type u} : Set α

The universal set on a type α is the set containing all elements of α.

This is conceptually the "same as" α (in set theory, it is actually the same), but type theory makes the distinction that α is a type while Set.univ is a term of type Set α. Set.univ can itself be coerced to a type ↥Set.univ which is in bijection with (but distinct from) α.

Equations

• Set.univ = {_a : α | True}

def Set.insert {α : Type u} (a : α) (s : Set α) : Set α

Set.insert a s is the set {a} ∪ s.

Note that you should not use this definition directly, but instead write insert a s (which is mediated by the Insert typeclass).

Equations

• Set.insert a s = {b : α | b = a ∨ b ∈ s}

instance Set.instInsert {α : Type u} : Insert α (Set α)

Equations

• Set.instInsert = { insert := Set.insert }

def Set.singleton {α : Type u} (a : α) : Set α

The singleton of an element a is the set with a as a single element.

Note that you should not use this definition directly, but instead write {a}.

Equations

• Set.singleton a = {b : α | b = a}

instance Set.instSingletonSet {α : Type u} : Singleton α (Set α)

Equations

• Set.instSingletonSet = { singleton := Set.singleton }

def Set.union {α : Type u} (s₁ : Set α) (s₂ : Set α) : Set α

The union of two sets s and t is the set of elements contained in either s or t.

Note that you should not use this definition directly, but instead write s ∪ t.

Equations

• s₁.union s₂ = {a : α | a ∈ s₁ ∨ a ∈ s₂}

instance Set.instUnion {α : Type u} : Union (Set α)

Equations

• Set.instUnion = { union := Set.union }

def Set.inter {α : Type u} (s₁ : Set α) (s₂ : Set α) : Set α

The intersection of two sets s and t is the set of elements contained in both s and t.

Note that you should not use this definition directly, but instead write s ∩ t.

Equations

• s₁.inter s₂ = {a : α | a ∈ s₁ ∧ a ∈ s₂}

instance Set.instInter {α : Type u} : Inter (Set α)

Equations

• Set.instInter = { inter := Set.inter }

def Set.compl {α : Type u} (s : Set α) : Set α

The complement of a set s is the set of elements not contained in s.

Note that you should not use this definition directly, but instead write sᶜ.

Equations

• s.compl = {a : α | ¬a ∈ s}

def Set.diff {α : Type u} (s : Set α) (t : Set α) : Set α

The difference of two sets s and t is the set of elements contained in s but not in t.

Note that you should not use this definition directly, but instead write s \ t.

Equations

• s.diff t = {a : α | a ∈ s ∧ ¬a ∈ t}

instance Set.instSDiff {α : Type u} : SDiff (Set α)

Equations

• Set.instSDiff = { sdiff := Set.diff }

def Set.powerset {α : Type u} (s : Set α) : Set (Set α)

𝒫 s is the set of all subsets of s.

Equations

• 𝒫 s = {t : Set α | t ⊆ s}

def Set.term𝒫_ : Lean.ParserDescr

𝒫 s is the set of all subsets of s.

Equations

• Set.term𝒫_ = Lean.ParserDescr.node `Set.term𝒫_ 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝒫") (Lean.ParserDescr.cat `term 100))

def Set.image {α : Type u} {β : Type v} (f : α → β) (s : Set α) : Set β

The image of s : Set α by f : α → β, written f '' s, is the set of b : β such that f a = b for some a ∈ s.

Equations

• Set.image f s = {x : β | ∃ (a : α), a ∈ s ∧ f a = x}

instance Set.instFunctor : Functor Set

Equations

• Set.instFunctor = { map := @Set.image, mapConst := fun {α β : Type u_1} => Set.image ∘ Function.const β }

instance Set.instLawfulFunctor : LawfulFunctor Set

Equations

• Set.instLawfulFunctor = ⋯

def Set.Nonempty {α : Type u} (s : Set α) : Prop

The property s.Nonempty expresses the fact that the set s is not empty. It should be used in theorem assumptions instead of ∃ x, x ∈ s or s ≠ ∅ as it gives access to a nice API thanks to the dot notation.

Equations

• s.Nonempty = ∃ (x : α), x ∈ s