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.

source

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)

Instances For

source

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

source

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

Prop

Membership in a set

Equations

s.Mem a = s a

source

instance Set.instMembership {α : Type u} :

Membership α (Set α)

Equations

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

source

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

a = b

source

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.

Equations

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

source

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 }

source

instance Set.instHasSubset {α : Type u} :

HasSubset (Set α)

Equations

Set.instHasSubset = { Subset := fun (x1 x2 : Set α) => x1 ≤ x2 }

source

instance Set.instEmptyCollection {α : Type u} :

EmptyCollection (Set α)

Equations

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

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

Equations

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

source

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.

source

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

Set.ordConnected_univ

source

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}

source

instance Set.instInsert {α : Type u} :

Insert α (Set α)

Equations

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

source

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}

source

instance Set.instSingletonSet {α : Type u} :

Singleton α (Set α)

Equations

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

source

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.

Equations

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

source

instance Set.instUnion {α : Type u} :

Union (Set α)

Equations

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

source

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.

Equations

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

source

instance Set.instInter {α : Type u} :

Inter (Set α)

Equations

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

source

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}

source

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.

Equations

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

source

instance Set.instSDiff {α : Type u} :

SDiff (Set α)

Equations

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

source

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

Set (Set α)

𝒫 s is the set of all subsets of s.

Equations

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

source

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

source

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}

Instances For

Set.ordConnected_image

source

instance Set.instFunctor :

Functor Set

Equations

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

source

instance Set.instLawfulFunctor :

LawfulFunctor Set

source

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

Documentation

Mathlib.Data.Set.Defs

Sets #

Main definitions #

Implementation issues #