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.

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

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

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

Membership in a set

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

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

def Set.Subset {α : Type u} (s₁ 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.

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

We introduce ≤ before ⊆ to help the unifier when applying lattice theorems to subset hypotheses.

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

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

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}.

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}.

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

Unexpander for set builder notation.

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)}.

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.

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.

def Mathlib.Meta.setOfPatternMatchUnexpander : Lean.PrettyPrinter.Unexpander

Pretty printing for set-builder notation with pattern matching.

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) α.

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).

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

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}.

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

def Set.union {α : Type u} (s₁ 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.

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

def Set.inter {α : Type u} (s₁ 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.

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

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ᶜ.

def Set.diff {α : Type u} (s 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.

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

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

𝒫 s is the set of all subsets of s.

def Set.term𝒫_ : Lean.ParserDescr

𝒫 s is the set of all subsets of s.

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.

instance Set.instFunctor : Functor Set

instance Set.instLawfulFunctor : LawfulFunctor Set

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.