# 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`

.

## Equations

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

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

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

Unexpander for set builder notation.

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

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

.

## Instances For

`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

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

`𝒫 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

## Equations

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

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.