# Note about `Mathlib/Init/`

#

The files in `Mathlib/Init`

are leftovers from the port from Mathlib3.
(They contain content moved from lean3 itself that Mathlib needed but was not moved to lean4.)

We intend to move all the content of these files out into the main `Mathlib`

directory structure.
Contributions assisting with this are appreciated.

# 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.instMembership = { mem := Set.Mem }

## 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.instFunctor = { 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.