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

I didn't call this file Data.Set.Basic because it contains core Lean 3
stuff which happens before mathlib3's data.set.basic .
This file is a port of the core Lean 3 file `lib/lean/library/init/data/set.lean`

.

## Equations

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

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

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

## Instances For

## Equations

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

## Instances For

## 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.instFunctorSet = { map := @Set.image, mapConst := fun {α β : Type u_1} => 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.

## Equations

- Set.Nonempty s = ∃ (x : α), x ∈ s