# 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) :

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
Instances For
def setOf {α : Type u} (p : αProp) :
Set α

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

Equations
Instances For
def Set.Mem {α : Type u} (a : α) (s : Set α) :

Membership in a set

Equations
Instances For
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 α) :

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₂
Instances For
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} :
Equations
• Set.instHasSubset = { Subset := fun (x x_1 : Set α) => x x_1 }
instance Set.instEmptyCollection {α : Type u} :
Equations
• Set.instEmptyCollection = { emptyCollection := fun (x : α) => False }
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For

{ 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.
Instances For
• { 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.
Instances For
• { 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.
Instances For

Pretty printing for set-builder notation with pattern matching.

Equations
• One or more equations did not get rendered due to their size.
Instances For
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}
Instances For
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
Instances For
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
• = {b : α | b = a}
Instances For
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₂}
Instances For
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₂}
Instances For
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}
Instances For
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
Instances For
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
Instances For

𝒫 s is the set of all subsets of s.

Equations
Instances For
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
• = {x : β | ∃ (a : α), a s f a = x}
Instances For
instance Set.instFunctor :
Equations
Equations
def Set.Nonempty {α : Type u} (s : Set α) :

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
Instances For