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 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 Mathlib.Meta.setBuilder : Lean.ParserDescr

Set builder syntax. This can be elaborated to either a Set or a Finset depending on context.

The elaborators for this syntax are located in:

• Data.Set.Defs for the Set builder notation elaborator for syntax of the form {x | p x}, {x : α | p x}, {binder x | p x}.
• Data.Finset.Basic for the Finset builder notation elaborator for syntax of the form {x ∈ s | p x}.
• Data.Fintype.Basic for the Finset builder notation elaborator for syntax of the form {x | p x}, {x : α | p x}, {x ∉ s | p x}, {x ≠ a | p x}.
• Order.LocallyFinite.Basic for the Finset builder notation elaborator for syntax of the form {x ≤ a | p x}, {x ≥ a | p x}, {x < a | p x}, {x > a | p x}.

Equations

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

def Mathlib.Meta.elabSetBuilder : Lean.Elab.Term.TermElab

Elaborate set builder notation for Set.

• {x | p x} is elaborated as Set.setOf fun x ↦ p x

• {x : α | p x} is elaborated as Set.setOf fun x : α ↦ p x

• {binder x | p x}, where x is bound by the binder binder, is elaborated as {x | binder x ∧ p x}. The typical example is {x ∈ s | p x}, which is elaborated as {x | x ∈ s ∧ p x}. The possible binders are

  • · ∈ s, · ∉ s
  • · ⊆ s, · ⊂ s, · ⊇ s, · ⊃ s
  • · ≤ a, · ≥ a, · < a, · > a, · ≠ a

  More binders can be declared using the binder_predicate command, see Init.BinderPredicates for more info.

See also

• Data.Finset.Basic for the Finset builder notation elaborator partly overriding this one for syntax of the form {x ∈ s | p x}.
• Data.Fintype.Basic for the Finset builder notation elaborator partly overriding this one for syntax of the form {x | p x}, {x : α | p x}, {x ∉ s | p x}, {x ≠ a | p x}.
• Order.LocallyFinite.Basic for the Finset builder notation elaborator partly overriding this one for syntax of the form {x ≤ a | p x}, {x ≥ a | p x}, {x < a | p x}, {x > a | p x}.

Equations

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

def Mathlib.Meta.setOf.unexpander : Lean.PrettyPrinter.Unexpander

Unexpander for set builder notation.

Equations

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

def Mathlib.Meta.«term{_|_}» : 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 Mathlib.Meta.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 Mathlib.Meta.«term{_|_}_1» : 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 Mathlib.Meta.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