mathlib3 documentation

def arity (α : Type u) :

ℕ → Type u

The type of n-ary functions α → α → ... → α.

Equations

arity α (n + 1) = (α → arity α n)
arity α 0 = α

Instances for arity

arity.arity.inhabited

@[simp]

theorem arity_zero (α : Type u) :

arity α 0 = α

@[simp]

theorem arity_succ (α : Type u) (n : ℕ) :

arity α n.succ = (α → arity α n)

def arity.const {α : Type u} (a : α) (n : ℕ) :

arity α n

Constant n-ary function with value a.

Equations

arity.const a (n + 1) = λ (_x : α), arity.const a n
arity.const a 0 = a

@[simp]

theorem arity.const_zero {α : Type u} (a : α) :

arity.const a 0 = a

@[simp]

theorem arity.const_succ {α : Type u} (a : α) (n : ℕ) :

arity.const a n.succ = λ (_x : α), arity.const a n

theorem arity.const_succ_apply {α : Type u} (a : α) (n : ℕ) (x : α) :

arity.const a n.succ x = arity.const a n

@[protected, instance]

def arity.arity.inhabited {α : Type u_1} {n : ℕ} [inhabited α] :

inhabited (arity α n)

Equations

arity.arity.inhabited = {default := arity.const inhabited.default n}

inductive pSet :

Type (u+1)

mk : Π (α : Type ?), (α → pSet) → pSet

The type of pre-sets in universe u. A pre-set is a family of pre-sets indexed by a type in Type u. The ZFC universe is defined as a quotient of this to ensure extensionality.

Instances for pSet

def pSet.type :

pSet → Type u

The underlying type of a pre-set

Equations

(pSet.mk α A).type = α

Instances for pSet.type

def pSet.func (x : pSet) :

x.type → pSet

The underlying pre-set family of a pre-set

Equations

(pSet.mk α A).func = A

@[simp]

theorem pSet.mk_type (α : Type u_1) (A : α → pSet) :

(pSet.mk α A).type = α

@[simp]

theorem pSet.mk_func (α : Type u_1) (A : α → pSet) :

(pSet.mk α A).func = A

@[simp]

theorem pSet.eta (x : pSet) :

pSet.mk x.type x.func = x

def pSet.equiv (x : pSet) (y : pSet) :

Prop

Two pre-sets are extensionally equivalent if every element of the first family is extensionally equivalent to some element of the second family and vice-versa.

Equations

x.equiv y = pSet.rec (λ (α : Type u_1) (z : α → pSet) (m : α → pSet → Prop) (_x : pSet), pSet.equiv._match_1 α m _x) x y
pSet.equiv._match_1 α m (pSet.mk β B) = ((∀ (a : α), ∃ (b : β), m a (B b)) ∧ ∀ (b : β), ∃ (a : α), m a (B b))

theorem pSet.equiv_iff {x : pSet} {y : pSet} :

x.equiv y ↔ (∀ (i : x.type), ∃ (j : y.type), (x.func i).equiv (y.func j)) ∧ ∀ (j : y.type), ∃ (i : x.type), (x.func i).equiv (y.func j)

theorem pSet.equiv.exists_left {x : pSet} {y : pSet} (h : x.equiv y) (i : x.type) :

∃ (j : y.type), (x.func i).equiv (y.func j)

theorem pSet.equiv.exists_right {x : pSet} {y : pSet} (h : x.equiv y) (j : y.type) :

∃ (i : x.type), (x.func i).equiv (y.func j)

@[protected, refl]

theorem pSet.equiv.refl (x : pSet) :

x.equiv x

@[protected]

theorem pSet.equiv.rfl {x : pSet} :

x.equiv x

@[protected]

theorem pSet.equiv.euc {x : pSet} {y : pSet} {z : pSet} :

x.equiv y → z.equiv y → x.equiv z

@[protected, symm]

theorem pSet.equiv.symm {x : pSet} {y : pSet} :

x.equiv y → y.equiv x

@[protected]

theorem pSet.equiv.comm {x : pSet} {y : pSet} :

x.equiv y ↔ y.equiv x

@[protected, trans]

theorem pSet.equiv.trans {x : pSet} {y : pSet} {z : pSet} (h1 : x.equiv y) (h2 : y.equiv z) :

x.equiv z

@[protected]

theorem pSet.equiv_of_is_empty (x : pSet) (y : pSet) [is_empty x.type] [is_empty y.type] :

x.equiv y

@[protected, instance]

def pSet.setoid :

setoid pSet

Equations

pSet.setoid = {r := pSet.equiv, iseqv := pSet.setoid._proof_1}

@[protected]

def pSet.subset (x : pSet) (y : pSet) :

Prop

A pre-set is a subset of another pre-set if every element of the first family is extensionally equivalent to some element of the second family.

Equations

x.subset y = ∀ (a : x.type), ∃ (b : y.type), (x.func a).equiv (y.func b)

@[protected, instance]

def pSet.has_subset :

has_subset pSet

Equations

pSet.has_subset = {subset := pSet.subset}

is_refl pSet has_subset.subset

@[protected, instance]

def pSet.has_subset.subset.is_refl :

is_trans pSet has_subset.subset

@[protected, instance]

def pSet.has_subset.subset.is_trans :

theorem pSet.equiv.ext (x y : pSet) :

x.equiv y ↔ x ⊆ y ∧ y ⊆ x

theorem pSet.subset.congr_left {x y z : pSet} :

x.equiv y → (x ⊆ z ↔ y ⊆ z)

theorem pSet.subset.congr_right {x y z : pSet} :

x.equiv y → (z ⊆ x ↔ z ⊆ y)

@[protected]

def pSet.mem (x y : pSet) :

Prop

x ∈ y as pre-sets if x is extensionally equivalent to a member of the family y.

Equations

x.mem y = ∃ (b : y.type), x.equiv (y.func b)

@[protected, instance]

def pSet.has_mem :

has_mem pSet pSet

Equations

pSet.has_mem = {mem := pSet.mem}

theorem pSet.mem.mk {α : Type u} (A : α → pSet) (a : α) :

A a ∈ pSet.mk α A

theorem pSet.func_mem (x : pSet) (i : x.type) :

x.func i ∈ x

theorem pSet.mem.ext {x y : pSet} :

(∀ (w : pSet), w ∈ x ↔ w ∈ y) → x.equiv y

theorem pSet.mem.congr_right {x y : pSet} :

x.equiv y → ∀ {w : pSet}, w ∈ x ↔ w ∈ y

theorem pSet.equiv_iff_mem {x y : pSet} :

x.equiv y ↔ ∀ {w : pSet}, w ∈ x ↔ w ∈ y

theorem pSet.mem.congr_left {x y : pSet} :

x.equiv y → ∀ {w : pSet}, x ∈ w ↔ y ∈ w

theorem pSet.mem_wf :

well_founded has_mem.mem

@[protected, instance]

def pSet.has_well_founded :

has_well_founded pSet

Equations

pSet.has_well_founded = {r := has_mem.mem pSet.has_mem, wf := pSet.mem_wf}

is_asymm pSet has_mem.mem

@[protected, instance]

def pSet.has_mem.mem.is_asymm :

theorem pSet.mem_asymm {x y : pSet} :

x ∈ y → y ∉ x

theorem pSet.mem_irrefl (x : pSet) :

x ∉ x

def pSet.to_set (u : pSet) :

set pSet

Convert a pre-set to a set of pre-sets.

Equations

u.to_set = {x : pSet | x ∈ u}

@[simp]

theorem pSet.mem_to_set (a u : pSet) :

a ∈ u.to_set ↔ a ∈ u

@[protected]

def pSet.nonempty (u : pSet) :

Prop

A nonempty set is one that contains some element.

Equations

u.nonempty = u.to_set.nonempty

theorem pSet.nonempty_def (u : pSet) :

u.nonempty ↔ ∃ (x : pSet), x ∈ u

theorem pSet.nonempty_of_mem {x u : pSet} (h : x ∈ u) :

u.nonempty

@[simp]

theorem pSet.nonempty_to_set_iff {u : pSet} :

u.to_set.nonempty ↔ u.nonempty

theorem pSet.nonempty_type_iff_nonempty {x : pSet} :

nonempty x.type ↔ x.nonempty

theorem pSet.nonempty_of_nonempty_type (x : pSet) [h : nonempty x.type] :

x.nonempty

theorem pSet.equiv.eq {x y : pSet} :

x.equiv y ↔ x.to_set = y.to_set

Two pre-sets are equivalent iff they have the same members.

@[protected, instance]

def pSet.set.has_coe :

has_coe pSet (set pSet)

Equations

pSet.set.has_coe = {coe := pSet.to_set}

@[protected]

def pSet.empty :

The empty pre-set

Equations

pSet.empty = pSet.mk pempty pempty.elim

@[protected, instance]

def pSet.has_emptyc :

has_emptyc pSet

Equations

pSet.has_emptyc = {emptyc := pSet.empty}

@[protected, instance]

def pSet.inhabited :

inhabited pSet

Equations

pSet.inhabited = {default := ∅}

@[protected, instance]

def pSet.type.is_empty :

is_empty ∅.type

@[simp]

theorem pSet.not_mem_empty (x : pSet) :

x ∉ ∅

@[simp]

theorem pSet.to_set_empty :

∅.to_set = ∅

@[simp]

theorem pSet.empty_subset (x : pSet) :

∅ ⊆ x

@[simp]

theorem pSet.not_nonempty_empty :

¬∅.nonempty

@[protected]

theorem pSet.equiv_empty (x : pSet) [is_empty x.type] :

x.equiv ∅

@[protected]

def pSet.insert (x y : pSet) :

Insert an element into a pre-set

Equations

x.insert y = pSet.mk (option y.type) (λ (o : option y.type), option.rec x y.func o)

@[protected, instance]

def pSet.has_insert :

has_insert pSet pSet

Equations

pSet.has_insert = {insert := pSet.insert}

@[protected, instance]

def pSet.has_singleton :

has_singleton pSet pSet

Equations

pSet.has_singleton = {singleton := λ (s : pSet), {s}}

is_lawful_singleton pSet pSet

@[protected, instance]

def pSet.is_lawful_singleton :

@[protected, instance]

def pSet.type.inhabited (x y : pSet) :

inhabited (has_insert.insert x y).type

Equations

pSet.type.inhabited x y = option.inhabited y.type

def pSet.of_nat :

ℕ → pSet

The n-th von Neumann ordinal

Equations

pSet.of_nat (n + 1) = has_insert.insert (pSet.of_nat n) (pSet.of_nat n)
pSet.of_nat 0 = ∅

def pSet.omega :

The von Neumann ordinal ω

Equations

pSet.omega = pSet.mk (ulift ℕ) (λ (n : ulift ℕ), pSet.of_nat n.down)

@[protected]

def pSet.sep (p : pSet → Prop) (x : pSet) :

The pre-set separation operation {x ∈ a | p x}

Equations

pSet.sep p x = pSet.mk {a // p (x.func a)} (λ (y : {a // p (x.func a)}), x.func y.val)

@[protected, instance]

def pSet.has_sep :

has_sep pSet pSet

Equations

pSet.has_sep = {sep := pSet.sep}

def pSet.powerset (x : pSet) :

The pre-set powerset operator

Equations

x.powerset = pSet.mk (set x.type) (λ (p : set x.type), pSet.mk {a // p a} (λ (y : {a // p a}), x.func y.val))

@[simp]

theorem pSet.mem_powerset {x y : pSet} :

y ∈ x.powerset ↔ y ⊆ x

def pSet.sUnion (a : pSet) :

The pre-set union operator

Equations

⋃₀ a = pSet.mk (Σ (x : a.type), (a.func x).type) (λ (_x : Σ (x : a.type), (a.func x).type), pSet.sUnion._match_1 a _x)
pSet.sUnion._match_1 a ⟨x, y⟩ = (a.func x).func y

@[simp]

theorem pSet.mem_sUnion {x y : pSet} :

y ∈ ⋃₀ x ↔ ∃ (z : pSet) (H : z ∈ x), y ∈ z

@[simp]

theorem pSet.to_set_sUnion (x : pSet) :

(⋃₀ x).to_set = ⋃₀ (pSet.to_set '' x.to_set)

def pSet.image (f : pSet → pSet) (x : pSet) :

The image of a function from pre-sets to pre-sets.

Equations

pSet.image f x = pSet.mk x.type (f ∘ x.func)

theorem pSet.mem_image {f : pSet → pSet} (H : ∀ {x y : pSet}, x.equiv y → (f x).equiv (f y)) {x y : pSet} :

y ∈ pSet.image f x ↔ ∃ (z : pSet) (H : z ∈ x), y.equiv (f z)

@[protected]

def pSet.lift :

pSet → pSet

Universe lift operation

Equations

(pSet.mk α A).lift = pSet.mk (ulift α) (λ (_x : ulift α), pSet.lift._match_1 α (λ (x : α), (A x).lift) _x)
pSet.lift._match_1 α _f_1 {down := x} = _f_1 x

@[nolint]

def pSet.embed :

Embedding of one universe in another

Equations

pSet.embed = pSet.mk (ulift pSet) (λ (_x : ulift pSet), pSet.embed._match_1 _x)
pSet.embed._match_1 {down := x} = x.lift

theorem pSet.lift_mem_embed (x : pSet) :

x.lift ∈ pSet.embed

def pSet.arity.equiv {n : ℕ} :

arity pSet n → arity pSet n → Prop

Function equivalence is defined so that f ~ g iff ∀ x y, x ~ y → f x ~ g y. This extends to equivalence of n-ary functions.

Equations

pSet.arity.equiv a b = ∀ (x y : pSet), x.equiv y → pSet.arity.equiv (a x) (b y)
pSet.arity.equiv a b = pSet.equiv a b

theorem pSet.arity.equiv_const {a : pSet} (n : ℕ) :

pSet.arity.equiv (arity.const a n) (arity.const a n)

def pSet.resp (n : ℕ) :

Type (u+1)

resp n is the collection of n-ary functions on pSet that respect equivalence, i.e. when the inputs are equivalent the output is as well.

Equations

pSet.resp n = {x // pSet.arity.equiv x x}

Instances for pSet.resp

@[protected, instance]

def pSet.resp.inhabited {n : ℕ} :

inhabited (pSet.resp n)

Equations

pSet.resp.inhabited = {default := ⟨arity.const inhabited.default n, _⟩}

def pSet.resp.f {n : ℕ} (f : pSet.resp (n + 1)) (x : pSet) :

pSet.resp n

The n-ary image of a (n + 1)-ary function respecting equivalence as a function respecting equivalence.

Equations

f.f x = ⟨f.val x, _⟩

def pSet.resp.equiv {n : ℕ} (a b : pSet.resp n) :

Prop

Function equivalence for functions respecting equivalence. See pSet.arity.equiv.

Equations

a.equiv b = pSet.arity.equiv a.val b.val

@[protected]

theorem pSet.resp.equiv.refl {n : ℕ} (a : pSet.resp n) :

a.equiv a

@[protected]

theorem pSet.resp.equiv.euc {n : ℕ} {a b c : pSet.resp n} :

a.equiv b → c.equiv b → a.equiv c

@[protected]

theorem pSet.resp.equiv.symm {n : ℕ} {a b : pSet.resp n} :

a.equiv b → b.equiv a

@[protected]

theorem pSet.resp.equiv.trans {n : ℕ} {x y z : pSet.resp n} (h1 : x.equiv y) (h2 : y.equiv z) :

x.equiv z

@[protected, instance]

def pSet.resp.setoid {n : ℕ} :

setoid (pSet.resp n)

Equations

pSet.resp.setoid = {r := pSet.resp.equiv n, iseqv := _}

def Set :

Type (u+1)

The ZFC universe of sets consists of the type of pre-sets, quotiented by extensional equivalence.

Equations

Set = quotient pSet.setoid

Instances for Set

def pSet.resp.eval_aux {n : ℕ} :

{f // ∀ (a b : pSet.resp n), a.equiv b → f a = f b}

Helper function for pSet.eval.

Equations

pSet.resp.eval_aux = let F : pSet.resp (n + 1) → arity Set (n + 1) := λ (a : pSet.resp (n + 1)), quotient.lift (λ (x : pSet), pSet.resp.eval_aux.val (a.f x)) _ in ⟨F, _⟩
pSet.resp.eval_aux = ⟨λ (a : pSet.resp 0), ⟦a.val ⟧, pSet.resp.eval_aux._main._proof_1⟩

def pSet.resp.eval (n : ℕ) :

pSet.resp n → arity Set n

An equivalence-respecting function yields an n-ary ZFC set function.

Equations

pSet.resp.eval n = pSet.resp.eval_aux.val

Instances for pSet.resp.eval

pSet.definable.mk

theorem pSet.resp.eval_val {n : ℕ} {f : pSet.resp (n + 1)} {x : pSet} :

pSet.resp.eval (n + 1) f ⟦x⟧ = pSet.resp.eval n (f.f x)

@[class]

inductive pSet.definable (n : ℕ) :

arity Set n → Type (u+1)

mk : Π {n : ℕ} (f : pSet.resp n), pSet.definable n (pSet.resp.eval n f)

A set function is "definable" if it is the image of some n-ary pre-set function. This isn't exactly definability, but is useful as a sufficient condition for functions that have a computable image.

Instances of this typeclass

Instances of other typeclasses for pSet.definable

pSet.definable.has_sizeof_inst

def pSet.definable.eq_mk {n : ℕ} (f : pSet.resp n) {s : arity Set n} (H : pSet.resp.eval n f = s) :

pSet.definable n s

The evaluation of a function respecting equivalence is definable, by that same function.

Equations

pSet.definable.eq_mk f rfl = pSet.definable.mk f

def pSet.definable.resp {n : ℕ} (s : arity Set n) [pSet.definable n s] :

pSet.resp n

Turns a definable function into a function that respects equivalence.

Equations

pSet.definable.resp (pSet.resp.eval n f) = f

theorem pSet.definable.eq {n : ℕ} (s : arity Set n) [H : pSet.definable n s] :

pSet.resp.eval n (pSet.definable.resp s) = s

noncomputable def classical.all_definable {n : ℕ} (F : arity Set n) :

pSet.definable n F

All functions are classically definable.

Equations

classical.all_definable F = pSet.definable.eq_mk ⟨λ (x : pSet), (pSet.definable.resp (F ⟦x⟧)).val, _⟩ _
classical.all_definable F = let p : ∃ (a : pSet), ⟦a⟧ = F := _ in pSet.definable.eq_mk ⟨classical.some p, _⟩ _

def Set.mk :

pSet → Set

Turns a pre-set into a ZFC set.

Equations

Set.mk = quotient.mk

@[simp]

theorem Set.mk_eq (x : pSet) :

⟦x⟧ = Set.mk x

@[simp]

theorem Set.mk_out (x : Set) :

Set.mk (quotient.out x) = x

theorem Set.eq {x y : pSet} :

Set.mk x = Set.mk y ↔ x.equiv y

theorem Set.sound {x y : pSet} (h : x.equiv y) :

Set.mk x = Set.mk y

theorem Set.exact {x y : pSet} :

Set.mk x = Set.mk y → x.equiv y

@[simp]

theorem Set.eval_mk {n : ℕ} {f : pSet.resp (n + 1)} {x : pSet} :

pSet.resp.eval (n + 1) f (Set.mk x) = pSet.resp.eval n (f.f x)

@[protected]

def Set.mem :

Set → Set → Prop

The membership relation for ZFC sets is inherited from the membership relation for pre-sets.

Equations

Set.mem = quotient.lift₂ pSet.mem Set.mem._proof_1

@[protected, instance]

def Set.has_mem :

has_mem Set Set

Equations

Set.has_mem = {mem := Set.mem}

@[simp]

theorem Set.mk_mem_iff {x y : pSet} :

Set.mk x ∈ Set.mk y ↔ x ∈ y

def Set.to_set (u : Set) :

set Set

Convert a ZFC set into a set of ZFC sets

Equations

u.to_set = {x : Set | x ∈ u}

Instances for ↥Set.to_set

Set.small_to_set

@[simp]

theorem Set.mem_to_set (a u : Set) :

a ∈ u.to_set ↔ a ∈ u

@[protected, instance]

def Set.small_to_set (x : Set) :

small ↥(x.to_set)

@[protected]

def Set.nonempty (u : Set) :

Prop

A nonempty set is one that contains some element.

Equations

u.nonempty = u.to_set.nonempty

theorem Set.nonempty_def (u : Set) :

u.nonempty ↔ ∃ (x : Set), x ∈ u

theorem Set.nonempty_of_mem {x u : Set} (h : x ∈ u) :

u.nonempty

@[simp]

theorem Set.nonempty_to_set_iff {u : Set} :

u.to_set.nonempty ↔ u.nonempty

@[protected]

def Set.subset (x y : Set) :

Prop

x ⊆ y as ZFC sets means that all members of x are members of y.

Equations

x.subset y = ∀ ⦃z : Set⦄, z ∈ x → z ∈ y

@[protected, instance]

def Set.has_subset :

has_subset Set

Equations

Set.has_subset = {subset := Set.subset}

theorem Set.subset_def {x y : Set} :

x ⊆ y ↔ ∀ ⦃z : Set⦄, z ∈ x → z ∈ y

is_refl Set has_subset.subset

@[protected, instance]

def Set.has_subset.subset.is_refl :

is_trans Set has_subset.subset

@[protected, instance]

def Set.has_subset.subset.is_trans :

@[simp]

theorem Set.subset_iff {x y : pSet} :

Set.mk x ⊆ Set.mk y ↔ x ⊆ y

@[simp]

theorem Set.to_set_subset_iff {x y : Set} :

x.to_set ⊆ y.to_set ↔ x ⊆ y

@[ext]

theorem Set.ext {x y : Set} :

(∀ (z : Set), z ∈ x ↔ z ∈ y) → x = y

theorem Set.ext_iff {x y : Set} :

x = y ↔ ∀ (z : Set), z ∈ x ↔ z ∈ y

function.injective Set.to_set

theorem Set.to_set_injective :

@[simp]

theorem Set.to_set_inj {x y : Set} :

x.to_set = y.to_set ↔ x = y

is_antisymm Set has_subset.subset

@[protected, instance]

def Set.has_subset.subset.is_antisymm :

@[protected]

def Set.empty :

The empty ZFC set

Equations

Set.empty = Set.mk ∅

@[protected, instance]

def Set.has_emptyc :

has_emptyc Set

Equations

Set.has_emptyc = {emptyc := Set.empty}

@[protected, instance]

def Set.inhabited :

inhabited Set

Equations

Set.inhabited = {default := ∅}

@[simp]

theorem Set.not_mem_empty (x : Set) :

x ∉ ∅

@[simp]

theorem Set.to_set_empty :

∅.to_set = ∅

@[simp]

theorem Set.empty_subset (x : Set) :

∅ ⊆ x

@[simp]

theorem Set.not_nonempty_empty :

¬∅.nonempty

@[simp]

theorem Set.nonempty_mk_iff {x : pSet} :

(Set.mk x).nonempty ↔ x.nonempty

theorem Set.eq_empty (x : Set) :

x = ∅ ↔ ∀ (y : Set), y ∉ x

theorem Set.eq_empty_or_nonempty (u : Set) :

u = ∅ ∨ u.nonempty

@[protected]

def Set.insert :

Set → Set → Set

insert x y is the set {x} ∪ y

Equations

Set.insert = pSet.resp.eval 2 ⟨pSet.insert, Set.insert._proof_1⟩

@[protected, instance]

def Set.has_insert :

has_insert Set Set

Equations

Set.has_insert = {insert := Set.insert}

@[protected, instance]

def Set.has_singleton :

has_singleton Set Set

Equations

Set.has_singleton = {singleton := λ (x : Set), {x}}

is_lawful_singleton Set Set

@[protected, instance]

def Set.is_lawful_singleton :

@[simp]

theorem Set.mem_insert_iff {x y z : Set} :

x ∈ has_insert.insert y z ↔ x = y ∨ x ∈ z

theorem Set.mem_insert (x y : Set) :

x ∈ has_insert.insert x y

theorem Set.mem_insert_of_mem {y z : Set} (x : Set) (h : z ∈ y) :

z ∈ has_insert.insert x y

@[simp]

theorem Set.to_set_insert (x y : Set) :

(has_insert.insert x y).to_set = has_insert.insert x y.to_set

@[simp]

theorem Set.mem_singleton {x y : Set} :

x ∈ {y} ↔ x = y

@[simp]

theorem Set.to_set_singleton (x : Set) :

{x}.to_set = {x}

theorem Set.insert_nonempty (u v : Set) :

(has_insert.insert u v).nonempty

theorem Set.singleton_nonempty (u : Set) :

{u}.nonempty

@[simp]

theorem Set.mem_pair {x y z : Set} :

x ∈ {y, z} ↔ x = y ∨ x = z

def Set.omega :

omega is the first infinite von Neumann ordinal

Equations

Set.omega = Set.mk pSet.omega

@[simp]

theorem Set.omega_zero :

∅ ∈ Set.omega

@[simp]

theorem Set.omega_succ {n : Set} :

n ∈ Set.omega → has_insert.insert n n ∈ Set.omega

@[protected]

def Set.sep (p : Set → Prop) :

{x ∈ a | p x} is the set of elements in a satisfying p

Equations

Set.sep p = pSet.resp.eval 1 ⟨pSet.sep (λ (y : pSet), p (Set.mk y)), _⟩

@[protected, instance]

def Set.has_sep :

has_sep Set Set

Equations

Set.has_sep = {sep := Set.sep}

@[simp]

theorem Set.mem_sep {p : Set → Prop} {x y : Set} :

y ∈ {y ∈ x | p y} ↔ y ∈ x ∧ p y

@[simp]

theorem Set.to_set_sep (a : Set) (p : Set → Prop) :

{x ∈ a | p x}.to_set = {x ∈ a.to_set | p x}

def Set.powerset :

The powerset operation, the collection of subsets of a ZFC set

Equations

Set.powerset = pSet.resp.eval 1 ⟨pSet.powerset, Set.powerset._proof_1⟩

@[simp]

theorem Set.mem_powerset {x y : Set} :

y ∈ x.powerset ↔ y ⊆ x

theorem Set.sUnion_lem {α β : Type u} (A : α → pSet) (B : β → pSet) (αβ : ∀ (a : α), ∃ (b : β), (A a).equiv (B b)) (a : (⋃₀ pSet.mk α A).type) :

∃ (b : (⋃₀ pSet.mk β B).type), ((⋃₀ pSet.mk α A).func a).equiv ((⋃₀ pSet.mk β B).func b)

def Set.sUnion :

The union operator, the collection of elements of elements of a ZFC set

Equations

Set.sUnion = pSet.resp.eval 1 ⟨pSet.sUnion, Set.sUnion._proof_1⟩

noncomputable def Set.sInter (x : Set) :

The intersection operator, the collection of elements in all of the elements of a ZFC set. We special-case ⋂₀ ∅ = ∅.

Equations

⋂₀ x = dite x.nonempty (λ (h : x.nonempty), {y ∈ set.nonempty.some h | ∀ (z : Set), z ∈ x → y ∈ z}) (λ (_x : ¬x.nonempty), ∅)

@[simp]

theorem Set.mem_sUnion {x y : Set} :

y ∈ ⋃₀ x ↔ ∃ (z : Set) (H : z ∈ x), y ∈ z

theorem Set.mem_sInter {x y : Set} (h : x.nonempty) :

y ∈ ⋂₀ x ↔ ∀ (z : Set), z ∈ x → y ∈ z

@[simp]

theorem Set.sUnion_empty :

⋃₀ ∅ = ∅

@[simp]

theorem Set.sInter_empty :

⋂₀ ∅ = ∅

theorem Set.mem_of_mem_sInter {x y z : Set} (hy : y ∈ ⋂₀ x) (hz : z ∈ x) :

y ∈ z

theorem Set.mem_sUnion_of_mem {x y z : Set} (hy : y ∈ z) (hz : z ∈ x) :

y ∈ ⋃₀ x

theorem Set.not_mem_sInter_of_not_mem {x y z : Set} (hy : y ∉ z) (hz : z ∈ x) :

y ∉ ⋂₀ x

@[simp]

theorem Set.sUnion_singleton {x : Set} :

⋃₀ {x} = x

@[simp]

theorem Set.sInter_singleton {x : Set} :

⋂₀ {x} = x

@[simp]

theorem Set.to_set_sUnion (x : Set) :

(⋃₀ x).to_set = ⋃₀ (Set.to_set '' x.to_set)

theorem Set.to_set_sInter {x : Set} (h : x.nonempty) :

(⋂₀ x).to_set = ⋂₀ (Set.to_set '' x.to_set)

function.injective has_singleton.singleton

theorem Set.singleton_injective :

@[simp]

theorem Set.singleton_inj {x y : Set} :

{x} = {y} ↔ x = y

@[protected]

def Set.union (x y : Set) :

The binary union operation

Equations

x.union y = ⋃₀ {x, y}

@[protected]

def Set.inter (x y : Set) :

The binary intersection operation

Equations

x.inter y = {z ∈ x | z ∈ y}

@[protected]

def Set.diff (x y : Set) :

The set difference operation

Equations

x.diff y = {z ∈ x | z ∉ y}

@[protected, instance]

def Set.has_union :

has_union Set

Equations

Set.has_union = {union := Set.union}

@[protected, instance]

def Set.has_inter :

has_inter Set

Equations

Set.has_inter = {inter := Set.inter}

@[protected, instance]

def Set.has_sdiff :

has_sdiff Set

Equations

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

@[simp]

theorem Set.to_set_union (x y : Set) :

(x ∪ y).to_set = x.to_set ∪ y.to_set

@[simp]

theorem Set.to_set_inter (x y : Set) :

(x ∩ y).to_set = x.to_set ∩ y.to_set

@[simp]

theorem Set.to_set_sdiff (x y : Set) :

(x \ y).to_set = x.to_set \ y.to_set

@[simp]

theorem Set.mem_union {x y z : Set} :

z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y

@[simp]

theorem Set.mem_inter {x y z : Set} :

z ∈ x ∩ y ↔ z ∈ x ∧ z ∈ y

@[simp]

theorem Set.mem_diff {x y z : Set} :

z ∈ x \ y ↔ z ∈ x ∧ z ∉ y

@[simp]

theorem Set.sUnion_pair {x y : Set} :

⋃₀ {x, y} = x ∪ y

theorem Set.mem_wf :

well_founded has_mem.mem

theorem Set.induction_on {p : Set → Prop} (x : Set) (h : ∀ (x : Set), (∀ (y : Set), y ∈ x → p y) → p x) :

p x

Induction on the ∈ relation.

@[protected, instance]

def Set.has_well_founded :

has_well_founded Set

Equations

Set.has_well_founded = {r := has_mem.mem Set.has_mem, wf := Set.mem_wf}

@[protected, instance]

def Set.has_mem.mem.is_asymm :

is_asymm Set has_mem.mem

theorem Set.mem_asymm {x y : Set} :

x ∈ y → y ∉ x

theorem Set.mem_irrefl (x : Set) :

x ∉ x

theorem Set.regularity (x : Set) (h : x ≠ ∅) :

∃ (y : Set) (H : y ∈ x), x ∩ y = ∅

def Set.image (f : Set → Set) [H : pSet.definable 1 f] :

The image of a (definable) ZFC set function

Equations

Set.image f = let r : pSet.resp 1 := pSet.definable.resp f in pSet.resp.eval 1 ⟨pSet.image r.val, _⟩

theorem Set.image.mk (f : Set → Set) [H : pSet.definable 1 f] (x : Set) {y : Set} (h : y ∈ x) :

f y ∈ Set.image f x

@[simp]

theorem Set.mem_image {f : Set → Set} [H : pSet.definable 1 f] {x y : Set} :

y ∈ Set.image f x ↔ ∃ (z : Set) (H : z ∈ x), f z = y

@[simp]

theorem Set.to_set_image (f : Set → Set) [H : pSet.definable 1 f] (x : Set) :

(Set.image f x).to_set = f '' x.to_set

noncomputable def Set.range {α : Type u} (f : α → Set) :

The range of an indexed family of sets. The universes allow for a more general index type without manual use of ulift.

Equations

Set.range f = ⟦pSet.mk (ulift α) (quotient.out ∘ f ∘ ulift.down)⟧

@[simp]

theorem Set.mem_range {α : Type u} {f : α → Set} {x : Set} :

x ∈ Set.range f ↔ x ∈ set.range f

@[simp]

theorem Set.to_set_range {α : Type u} (f : α → Set) :

(Set.range f).to_set = set.range f

def Set.pair (x y : Set) :

Kuratowski ordered pair

Equations

x.pair y = {{x}, {x, y}}

Instances for Set.pair

Set.map_definable_aux

@[simp]

theorem Set.to_set_pair (x y : Set) :

(x.pair y).to_set = {{x}, {x, y}}

def Set.pair_sep (p : Set → Set → Prop) (x y : Set) :

A subset of pairs {(a, b) ∈ x × y | p a b}

Equations

Set.pair_sep p x y = {z ∈ (x ∪ y).powerset.powerset | ∃ (a : Set) (H : a ∈ x) (b : Set) (H : b ∈ y), z = a.pair b ∧ p a b}

@[simp]

theorem Set.mem_pair_sep {p : Set → Set → Prop} {x y z : Set} :

z ∈ Set.pair_sep p x y ↔ ∃ (a : Set) (H : a ∈ x) (b : Set) (H : b ∈ y), z = a.pair b ∧ p a b

function.injective2 Set.pair

theorem Set.pair_injective :

@[simp]

theorem Set.pair_inj {x y x' y' : Set} :

x.pair y = x'.pair y' ↔ x = x' ∧ y = y'

def Set.prod :

Set → Set → Set

The cartesian product, {(a, b) | a ∈ x, b ∈ y}

Equations

Set.prod = Set.pair_sep (λ (a b : Set), true)

@[simp]

theorem Set.mem_prod {x y z : Set} :

z ∈ x.prod y ↔ ∃ (a : Set) (H : a ∈ x) (b : Set) (H : b ∈ y), z = a.pair b

@[simp]

theorem Set.pair_mem_prod {x y a b : Set} :

a.pair b ∈ x.prod y ↔ a ∈ x ∧ b ∈ y

def Set.is_func (x y f : Set) :

Prop

is_func x y f is the assertion that f is a subset of x × y which relates to each element of x a unique element of y, so that we can consider fas a ZFC function x → y.

Equations

x.is_func y f = (f ⊆ x.prod y ∧ ∀ (z : Set), z ∈ x → (∃! (w : Set), z.pair w ∈ f))

def Set.funs (x y : Set) :

funs x y is y ^ x, the set of all set functions x → y

Equations

x.funs y = {f ∈ (x.prod y).powerset | x.is_func y f}

@[simp]

theorem Set.mem_funs {x y f : Set} :

f ∈ x.funs y ↔ x.is_func y f

@[protected, instance]

noncomputable def Set.map_definable_aux (f : Set → Set) [H : pSet.definable 1 f] :

pSet.definable 1 (λ (y : Set), y.pair (f y))

Equations

Set.map_definable_aux f = classical.all_definable (λ (y : Set), y.pair (f y))

noncomputable def Set.map (f : Set → Set) [H : pSet.definable 1 f] :

Graph of a function: map f x is the ZFC function which maps a ∈ x to f a

Equations

Set.map f = Set.image (λ (y : Set), y.pair (f y))

@[simp]

theorem Set.mem_map {f : Set → Set} [H : pSet.definable 1 f] {x y : Set} :

y ∈ Set.map f x ↔ ∃ (z : Set) (H : z ∈ x), z.pair (f z) = y

theorem Set.map_unique {f : Set → Set} [H : pSet.definable 1 f] {x z : Set} (zx : z ∈ x) :

∃! (w : Set), z.pair w ∈ Set.map f x

@[simp]

theorem Set.map_is_func {f : Set → Set} [H : pSet.definable 1 f] {x y : Set} :

x.is_func y (Set.map f x) ↔ ∀ (z : Set), z ∈ x → f z ∈ y

def Set.hereditarily (p : Set → Prop) :

Set → Prop

Given a predicate p on ZFC sets. hereditarily p x means that x has property p and the members of x are all hereditarily p.

Equations

Set.hereditarily p x = (p x ∧ ∀ (y : Set), y ∈ x → Set.hereditarily p y)

theorem Set.hereditarily_iff {p : Set → Prop} {x : Set} :

Set.hereditarily p x ↔ p x ∧ ∀ (y : Set), y ∈ x → Set.hereditarily p y

theorem Set.hereditarily.def {p : Set → Prop} {x : Set} :

Set.hereditarily p x → (p x ∧ ∀ (y : Set), y ∈ x → Set.hereditarily p y)

Alias of the forward direction of Set.hereditarily_iff.

theorem Set.hereditarily.self {p : Set → Prop} {x : Set} (h : Set.hereditarily p x) :

p x

theorem Set.hereditarily.mem {p : Set → Prop} {x y : Set} (h : Set.hereditarily p x) (hy : y ∈ x) :

Set.hereditarily p y

theorem Set.hereditarily.empty {p : Set → Prop} {x : Set} :

Set.hereditarily p x → p ∅

@[protected, instance]

def Class.has_inter :

has_inter Class

@[protected, instance]

def Class.has_subset :

has_subset Class

@[protected, instance]

def Class.has_sdiff :

has_sdiff Class

@[protected, instance]

def Class.has_sep :

has_sep Set Class

def Class :

Type (u_1+1)

The collection of all classes.

We define Class as set Set, as this allows us to get many instances automatically. However, in practice, we treat it as (the definitionally equal) Set → Prop. This means, the preferred way to state that x : Set belongs to A : Class is to write A x.

Equations

Class = set Set

Instances for Class

@[protected, instance]

def Class.has_compl :

has_compl Class

@[protected, instance]

def Class.has_union :

has_union Class

@[protected, instance]

def Class.has_emptyc :

has_emptyc Class

@[protected, instance]

def Class.has_insert :

has_insert Set Class

@[protected, instance]

def Class.inhabited :

inhabited Class

@[ext]

theorem Class.ext {x y : Class} :

(∀ (z : Set), x z ↔ y z) → x = y

theorem Class.ext_iff {x y : Class} :

x = y ↔ ∀ (z : Set), x z ↔ y z

def Class.of_Set (x : Set) :

Coerce a ZFC set into a class

Equations

Class.of_Set x = {y : Set | y ∈ x}

@[protected, instance]

def Class.has_coe :

has_coe Set Class

Equations

Class.has_coe = {coe := Class.of_Set}

def Class.univ :

The universal class

Equations

Class.univ = set.univ

def Class.to_Set (B A : Class) :

Prop

Assert that A is a ZFC set satisfying B

Equations

B.to_Set A = ∃ (x : Set), ↑x = A ∧ B x

@[protected]

def Class.mem (A B : Class) :

Prop

A ∈ B if A is a ZFC set which satisfies B

Equations

A.mem B = B.to_Set A

@[protected, instance]

def Class.has_mem :

has_mem Class Class

Equations

Class.has_mem = {mem := Class.mem}

theorem Class.mem_def (A B : Class) :

A ∈ B ↔ ∃ (x : Set), ↑x = A ∧ B x

@[simp]

theorem Class.not_mem_empty (x : Class) :

x ∉ ∅

@[simp]

theorem Class.not_empty_hom (x : Set) :

¬∅ x

@[simp]

theorem Class.mem_univ {A : Class} :

A ∈ Class.univ ↔ ∃ (x : Set), ↑x = A

@[simp]

theorem Class.mem_univ_hom (x : Set) :

Class.univ x

theorem Class.eq_univ_iff_forall {A : Class} :

A = Class.univ ↔ ∀ (x : Set), A x

theorem Class.eq_univ_of_forall {A : Class} :

(∀ (x : Set), A x) → A = Class.univ

theorem Class.mem_wf :

well_founded has_mem.mem

@[protected, instance]

def Class.has_well_founded :

has_well_founded Class

Equations

Class.has_well_founded = {r := has_mem.mem Class.has_mem, wf := Class.mem_wf}

is_asymm Class has_mem.mem

@[protected, instance]

def Class.has_mem.mem.is_asymm :

theorem Class.mem_asymm {x y : Class} :

x ∈ y → y ∉ x

theorem Class.mem_irrefl (x : Class) :

x ∉ x

theorem Class.univ_not_mem_univ :

Class.univ ∉ Class.univ

There is no universal set.

This is stated as univ ∉ univ, meaning that univ (the class of all sets) is proper (does not belong to the class of all sets).

def Class.Cong_to_Class (x : set Class) :

Convert a conglomerate (a collection of classes) into a class

Equations

Class.Cong_to_Class x = {y : Set | ↑y ∈ x}

@[simp]

theorem Class.Cong_to_Class_empty :

Class.Cong_to_Class ∅ = ∅

def Class.Class_to_Cong (x : Class) :

set Class

Convert a class into a conglomerate (a collection of classes)

Equations

x.Class_to_Cong = {y : Class | y ∈ x}

@[simp]

theorem Class.Class_to_Cong_empty :

∅.Class_to_Cong = ∅

def Class.powerset (x : Class) :

The power class of a class is the class of all subclasses that are ZFC sets

Equations

x.powerset = Class.Cong_to_Class (𝒫x)

def Class.sUnion (x : Class) :

The union of a class is the class of all members of ZFC sets in the class

Equations

⋃₀ x = ⋃₀ x.Class_to_Cong

def Class.sInter (x : Class) :

The intersection of a class is the class of all members of ZFC sets in the class

Equations

⋂₀ x = ⋂₀ x.Class_to_Cong

theorem Class.of_Set.inj {x y : Set} (h : ↑x = ↑y) :

x = y

@[simp]

theorem Class.to_Set_of_Set (A : Class) (x : Set) :

A.to_Set ↑x ↔ A x

@[simp, norm_cast]

theorem Class.coe_mem {x : Set} {A : Class} :

↑x ∈ A ↔ A x

@[simp]

theorem Class.coe_apply {x y : Set} :

↑y x ↔ x ∈ y

@[simp, norm_cast]

theorem Class.coe_subset (x y : Set) :

↑x ⊆ ↑y ↔ x ⊆ y

@[simp, norm_cast]

theorem Class.coe_sep (p : Class) (x : Set) :

↑{y ∈ x | p y} = {y ∈ ↑x | p y}

@[simp, norm_cast]

theorem Class.coe_empty :

↑∅ = ∅

@[simp, norm_cast]

theorem Class.coe_insert (x y : Set) :

↑(has_insert.insert x y) = has_insert.insert x ↑y

@[simp, norm_cast]

theorem Class.coe_union (x y : Set) :

↑(x ∪ y) = ↑x ∪ ↑y

@[simp, norm_cast]

theorem Class.coe_inter (x y : Set) :

↑(x ∩ y) = ↑x ∩ ↑y

@[simp, norm_cast]

theorem Class.coe_diff (x y : Set) :

↑(x \ y) = ↑x \ ↑y

@[simp, norm_cast]

theorem Class.coe_powerset (x : Set) :

↑(x.powerset) = ↑x.powerset

@[simp]

theorem Class.powerset_apply {A : Class} {x : Set} :

A.powerset x ↔ ↑x ⊆ A

@[simp]

theorem Class.sUnion_apply {x : Class} {y : Set} :

(⋃₀ x) y ↔ ∃ (z : Set), x z ∧ y ∈ z

@[simp, norm_cast]

theorem Class.coe_sUnion (x : Set) :

↑⋃₀ x = ⋃₀ ↑x

@[simp]

theorem Class.mem_sUnion {x y : Class} :

y ∈ ⋃₀ x ↔ ∃ (z : Class), z ∈ x ∧ y ∈ z

@[simp]

theorem Class.sInter_apply {x : Class} {y : Set} :

(⋂₀ x) y ↔ ∀ (z : Set), x z → y ∈ z

@[simp, norm_cast]

theorem Class.coe_sInter {x : Set} (h : x.nonempty) :

↑⋂₀ x = ⋂₀ ↑x

theorem Class.mem_of_mem_sInter {x y z : Class} (hy : y ∈ ⋂₀ x) (hz : z ∈ x) :

y ∈ z

theorem Class.mem_sInter {x y : Class} (h : set.nonempty x) :

y ∈ ⋂₀ x ↔ ∀ (z : Class), z ∈ x → y ∈ z

@[simp]

theorem Class.sUnion_empty :

⋃₀ ∅ = ∅

@[simp]

theorem Class.sInter_empty :

⋂₀ ∅ = Class.univ

theorem Class.eq_univ_of_powerset_subset {A : Class} (hA : A.powerset ⊆ A) :

A = Class.univ

An induction principle for sets. If every subset of a class is a member, then the class is universal.

def Class.iota (A : Class) :

The definite description operator, which is {x} if {y | A y} = {x} and ∅ otherwise.

Equations

A.iota = ⋃₀ {x : Set | ∀ (y : Set), A y ↔ y = x}

theorem Class.iota_val (A : Class) (x : Set) (H : ∀ (y : Set), A y ↔ y = x) :

A.iota = ↑x

theorem Class.iota_ex (A : Class) :

A.iota ∈ Class.univ

Unlike the other set constructors, the iota definite descriptor is a set for any set input, but not constructively so, so there is no associated Class → Set function.

def Class.fval (F A : Class) :