# 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

Instances For

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

Membership in a set

Equations

- s.Mem a = s a

Instances For

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
theorem Set.ext_iff {α : Type u} {a b : Set α} :
a = b ↔ ∀ (x : α), x ∈ a ↔ x ∈ 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₂

Instances For

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

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.

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

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.

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

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.

Instances For

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

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}

Instances For

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}

Instances For

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

Instances For

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

Instances For

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}

Instances For

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}

Instances For

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}

Instances For

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

Instances For

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

source
instance Set.instFunctor :
Functor Set
Equations

- Set.instFunctor = { map := @Set.image }

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

Instances For