set_theory.zfc

A model of ZFC #

In this file, we model Zermelo-Fraenkel set theory (+ Choice) using Lean's underlying type theory. We do this in four main steps:

• Define pre-sets inductively.
• Define extensional equivalence on pre-sets and give it a setoid instance.
• Define ZFC sets by quotienting pre-sets by extensional equivalence.
• Define classes as sets of ZFC sets. Then the rest is usual set theory.

The model #

• pSet: Pre-set. A pre-set is inductively defined by its indexing type and its members, which are themselves pre-sets.
• Set: ZFC set. Defined as pSet quotiented by pSet.equiv, the extensional equivalence.
• Class: Class. Defined as set Set.
• Set.choice: Axiom of choice. Proved from Lean's axiom of choice.

Other definitions #

• arity α n: n-ary function α → α → ... → α. Defined inductively.
• arity.const a n: n-ary constant function equal to a.
• pSet.type: Underlying type of a pre-set.
• pSet.func: Underlying family of pre-sets of a pre-set.
• pSet.equiv: Extensional equivalence of pre-sets. Defined inductively.
• pSet.omega, Set.omega: The von Neumann ordinal ω as a pSet, as a Set.
• pSet.arity.equiv: Extensional equivalence of n-ary pSet-valued functions. Extension of pSet.equiv.
• pSet.resp: Collection of n-ary pSet-valued functions that respect extensional equivalence.
• pSet.eval: Turns a pSet-valued function that respect extensional equivalence into a Set-valued function.
• classical.all_definable: All functions are classically definable.
• Set.is_func : Predicate that a ZFC set is a subset of x × y that can be considered as a ZFC function x → y. That is, each member of x is related by the ZFC set to exactly one member of y.
• Set.funs: ZFC set of ZFC functions x → y.
• Class.iota: Definite description operator.

Notes #

To avoid confusion between the Lean set and the ZFC Set, docstrings in this file refer to them respectively as "set" and "ZFC set".

TODO #

Prove Set.map_definable_aux computably.

def arity (α : Type u) :
Type u

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

Equations
• (n + 1) = (α → n)
• 0 = α
Instances for arity
@[simp]
theorem arity_zero (α : Type u) :
0 = α
Informal translation

The arity of a type $α$ with $0$ arguments is $α$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem arity_succ (α : Type u) (n : ) :
n.succ = (α → n)
Informal translation

The arity of a function of arity $n+1$ is the arity of a function of arity $n$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
def arity.const {α : Type u} (a : α) (n : ) :
n

Constant n-ary function with value a.

Equations
• (n + 1) = λ (_x : α), n
• 0 = a
@[simp]
theorem arity.const_zero {α : Type u} (a : α) :
0 = a
Informal translation

The constant function $f(x_1,\ldots,x_n)=a$ is equal to $a$ when $n=0$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem arity.const_succ {α : Type u} (a : α) (n : ) :
n.succ = λ (_x : α), n
Informal translation

Let $a$ be an element of a type $α$ and let $n$ be a natural number. Then the function $f:\alpha\to\alpha$ defined by $f(x)=a$ for all $x\in\alpha$ is equal to the function $g:\alpha\to\alpha$ defined by $g(x)=a$ for all $x\in\alpha$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem arity.const_succ_apply {α : Type u} (a : α) (n : ) (x : α) :
n.succ x = n
Informal translation

Let $a$ be an element of a type $α$ and let $n$ be a natural number. Then $arity.const a (n+1) x = arity.const a n$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected, instance]
def arity.arity.inhabited {α : Type u_1} {n : } [inhabited α] :
Equations
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  :
pSetType u

The underlying type of a pre-set

Equations
Instances for pSet.type
def pSet.func (x : pSet) :
x.typepSet

The underlying pre-set family of a pre-set

Equations
@[simp]
theorem pSet.mk_type (α : Type u_1) (A : α → pSet) :
(pSet.mk α A).type = α
Informal translation

The type of the pSet $pSet.mk α A$ is $α$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem pSet.mk_func (α : Type u_1) (A : α → pSet) :
(pSet.mk α A).func = A
Informal translation

The function of the power set of a set $A$ is $A$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem pSet.eta (x : pSet) :
x.func = x
Informal translation

The map $\eta: \mathrm{pSet}\to \mathrm{pSet}$ is the identity map.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
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.exists_equiv_left {x : pSet} {y : pSet} (h : x.equiv y) (i : x.type) :
∃ (j : y.type), (x.func i).equiv (y.func j)
Informal translation

Let $x$ and $y$ be pointed sets. If $x$ and $y$ are equivalent, then for each $i\in x$ there is a $j\in y$ such that $x(i)$ and $y(j)$ are equivalent.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem pSet.exists_equiv_right {x : pSet} {y : pSet} (h : x.equiv y) (j : y.type) :
∃ (i : x.type), (x.func i).equiv (y.func j)
Informal translation

Let $x$ and $y$ be pointed sets. If $x$ and $y$ are equivalent, then there is a pointed set $z$ such that $x$ and $z$ are equivalent and $y$ and $z$ are equivalent.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected]
theorem pSet.equiv.refl (x : pSet) :
x.equiv x
Informal translation

The identity function is an equivalence of $x$ with itself.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected]
theorem pSet.equiv.rfl {x : pSet} :
x.equiv x
Informal translation

The identity function is an equivalence of $x$ with itself.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected]
theorem pSet.equiv.euc {x : pSet} {y : pSet} {z : pSet} :
x.equiv yz.equiv yx.equiv z
Informal translation

If $x$ is equivalent to $y$ and $y$ is equivalent to $z$, then $x$ is equivalent to $z$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected]
theorem pSet.equiv.symm {x : pSet} {y : pSet} :
x.equiv yy.equiv x
Informal translation

If $x$ and $y$ are equivalent posets, then $y$ and $x$ are equivalent posets.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected]
theorem pSet.equiv.trans {x : pSet} {y : pSet} {z : pSet} (h1 : x.equiv y) (h2 : y.equiv z) :
x.equiv z
Informal translation

If $x$ is equinumerous to $y$ and $y$ is equinumerous to $z$, then $x$ is equinumerous to $z$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected, instance]
Equations
@[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
@[protected, instance]
Equations
theorem pSet.equiv.ext (x y : pSet) :
x.equiv y x y y x
Informal translation

Two sets $x$ and $y$ are equivalent if and only if $x\subset y$ and $y\subset x$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem pSet.subset.congr_left {x y z : pSet} :
x.equiv y(x z y z)
Informal translation

Let $x,y,z$ be pSets. If $x$ and $y$ are equivalent, then $x\subset z$ if and only if $y\subset z$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem pSet.subset.congr_right {x y z : pSet} :
x.equiv y(z x z y)
Informal translation

Let $x,y,z$ be pointed sets. If $x$ and $y$ are equivalent, then $z\subset x$ if and only if $z\subset y$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[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
@[protected, instance]
Equations
theorem pSet.mem.mk {α : Type u} (A : α → pSet) (a : α) :
A a A
Informal translation

Let $A$ be a function from a set $X$ to the power set of $X$. Then $A(x)\in\mathcal{P}(X)$ for all $x\in X$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem pSet.mem.ext {x y : pSet} :
(∀ (w : pSet), w x w y)x.equiv y
Informal translation

Two sets $x$ and $y$ are equal if and only if they have the same elements.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem pSet.mem.congr_right {x y : pSet} :
x.equiv y∀ {w : pSet}, w x w y
Informal translation

If $x$ and $y$ are equivalent sets, then $w\in x$ if and only if $w\in y$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem pSet.equiv_iff_mem {x y : pSet} :
x.equiv y ∀ {w : pSet}, w x w y
Informal translation

Two sets $x$ and $y$ are equivalent if and only if $w\in x$ if and only if $w\in y$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem pSet.mem.congr_left {x y : pSet} :
x.equiv y∀ {w : pSet}, x w y w
Informal translation

If $x$ and $y$ are equivalent sets, then $x\in w$ if and only if $y\in w$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem pSet.mem_wf  :
Informal translation

The membership relation on the set of all sets is well-founded.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected, instance]
Equations
@[protected, instance]
theorem pSet.mem_asymm {x y : pSet} :
x yy x
Informal translation

If $x$ is a member of $y$, then $y$ is not a member of $x$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem pSet.mem_irrefl (x : pSet) :
x x
Informal translation

The partial set $x$ is not a member of itself.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
def pSet.to_set (u : pSet) :

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

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

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

Informal translation

Two pSets $x$ and $y$ are equivalent if and only if their underlying sets are equal.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected, instance]
Equations
@[protected]
def pSet.empty  :

The empty pre-set

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[simp]
theorem pSet.mem_empty (x : pSet) :
Informal translation

No element of a pSet is in the empty set.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem pSet.empty_subset (x : pSet) :
Informal translation

The empty set is a subset of any set.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected]
def pSet.insert (x y : pSet) :

Insert an element into a pre-set

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
def pSet.type.inhabited (x y : pSet) :
Equations
def pSet.of_nat  :

The n-th von Neumann ordinal

Equations
def pSet.omega  :

The von Neumann ordinal ω

Equations
@[protected]
def pSet.sep (p : pSet → Prop) (x : pSet) :

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

Equations
@[protected, instance]
Equations
def pSet.powerset (x : pSet) :

The pre-set powerset operator

Equations
@[simp]
theorem pSet.mem_powerset {x y : pSet} :
Informal translation

Let $x$ and $y$ be sets. Then $y\in x^*$ if and only if $y\subset x$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
def pSet.sUnion (a : pSet) :

The pre-set union operator

Equations
@[simp]
theorem pSet.mem_sUnion {x y : pSet} :
y ⋃₀ x ∃ (z : pSet) (H : z x), y z
Informal translation

Let $x$ and $y$ be pSets. Then $y\in\bigcup x$ if and only if there is a pSet $z$ such that $z\in x$ and $y\in z$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
def pSet.image (f : pSetpSet) (x : pSet) :

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

Equations
theorem pSet.mem_image {f : pSetpSet} (H : ∀ {x y : pSet}, x.equiv y(f x).equiv (f y)) {x y : pSet} :
y x ∃ (z : pSet) (H : z x), y.equiv (f z)
Informal translation

Let $f:X\to Y$ be a function between two sets $X$ and $Y$. Then $y\in f(X)$ if and only if there is an $x\in X$ such that $y=f(x)$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected]
def pSet.lift  :

Universe lift operation

Equations
@[nolint]
def pSet.embed  :

Embedding of one universe in another

Equations
theorem pSet.lift_mem_embed (x : pSet) :
Informal translation

The lift of a pSet is in the embedding of pSet.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
def pSet.arity.equiv {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
theorem pSet.arity.equiv_const {a : pSet} (n : ) :
n)
Informal translation

The arity of a constant function is constant.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
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
• = {x // x}
Instances for pSet.resp
@[protected, instance]
def pSet.resp.inhabited {n : } :
Equations
def pSet.resp.f {n : } (f : pSet.resp (n + 1)) (x : pSet) :

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

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

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

Equations
@[protected]
theorem pSet.resp.equiv.refl {n : } (a : pSet.resp n) :
a.equiv a
Informal translation

The relation of being equivalent is reflexive on the set of partitions of $n$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected]
theorem pSet.resp.equiv.euc {n : } {a b c : pSet.resp n} :
a.equiv bc.equiv ba.equiv c
Informal translation

Let $a,b,c$ be partitions of a set of size $n$. If $a$ and $b$ are equivalent and $b$ and $c$ are equivalent, then $a$ and $c$ are equivalent.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected]
theorem pSet.resp.equiv.symm {n : } {a b : pSet.resp n} :
a.equiv bb.equiv a
Informal translation

Let $a$ and $b$ be partitions of a set of size $n$. Then $a$ is equivalent to $b$ if and only if $b$ is equivalent to $a$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected]
theorem pSet.resp.equiv.trans {n : } {x y z : pSet.resp n} (h1 : x.equiv y) (h2 : y.equiv z) :
x.equiv z
Informal translation

Let $n$ be a natural number and let $x, y, z$ be $n$-element sets. If $x$ is equivalent to $y$ and $y$ is equivalent to $z$, then $x$ is equivalent to $z$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected, instance]
Equations
def Set  :
Type (u+1)

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

Equations
Instances for Set
def pSet.resp.eval_aux {n : } :
{f // ∀ (a b : , a.equiv bf a = f b}

Helper function for pSet.eval.

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

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

Equations
Instances for pSet.resp.eval
theorem pSet.resp.eval_val {n : } {f : pSet.resp (n + 1)} {x : pSet} :
pSet.resp.eval (n + 1) f x = (f.f x)
Informal translation

Let $f$ be a function from $n+1$-types to sets. Then $f(x)$ is a function from $n$-types to sets.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[class]
inductive pSet.definable (n : ) :
nType (u+1)
• mk : Π {n : } (f : , 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 : n} (H : = s) :

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

Equations
def pSet.definable.resp {n : } (s : n) [ s] :

Turns a definable function into a function that respects equivalence.

Equations
theorem pSet.definable.eq {n : } (s : n) [H : s] :
Informal translation

The definable set $s$ is equal to the set $pSet.resp.eval n (pSet.definable.resp s)$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
noncomputable def classical.all_definable {n : } (F : n) :

All functions are classically definable.

Equations
def Set.mk  :

Turns a pre-set into a ZFC set.

Equations
@[simp]
theorem Set.mk_eq (x : pSet) :
Informal translation

The set of all sets is equal to the set of all sets.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Set.mk_out (x : Set) :
= x
Informal translation

The set of equivalence classes of $x$ is $x$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem Set.eq {x y : pSet} :
= x.equiv y
Informal translation

Two sets $x$ and $y$ are equal if and only if they are equivalent.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem Set.sound {x y : pSet} (h : x.equiv y) :
=
Informal translation

If $x$ and $y$ are equivalent sets, then $x=y$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem Set.exact {x y : pSet} :
= x.equiv y
Informal translation

If two sets $x$ and $y$ have the same underlying type, then they are equal.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Set.eval_mk {n : } {f : pSet.resp (n + 1)} {x : pSet} :
pSet.resp.eval (n + 1) f (Set.mk x) = (f.f x)
Informal translation

Let $n$ be a natural number and let $f$ be a function from $n+1$-element sets to sets. Let $x$ be a set. Then $f(x\cup\{x\})=f(x)$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected]
def Set.mem  :
SetSet → Prop

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

Equations
@[protected, instance]
def Set.has_mem  :
Equations
def Set.to_set (u : Set) :

Convert a ZFC set into a set of ZFC sets

Equations
@[protected]
def Set.subset (x y : Set) :
Prop

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

Equations
@[protected, instance]
Equations
theorem Set.subset_def {x y : Set} :
x y ∀ ⦃z : Set⦄, z xz y
Informal translation

$x\subseteq y$ if and only if $z\in x$ implies $z\in y$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Set.subset_iff {x y : pSet} :
x y
Informal translation

Let $x$ and $y$ be sets. Then $x\subset y$ if and only if $Set.mk x\subset Set.mk y$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem Set.ext {x y : Set} :
(∀ (z : Set), z x z y)x = y
Informal translation

Two sets $x$ and $y$ are equal if and only if they contain the same elements.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem Set.ext_iff {x y : Set} :
(∀ (z : Set), z x z y) x = y
Informal translation

Two sets $x$ and $y$ are equal if and only if they contain the same elements.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected]
def Set.empty  :

The empty ZFC set

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem Set.mem_empty (x : Set) :
Informal translation

$x$ is not an element of the empty set.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Set.empty_subset (x : Set) :
Informal translation

The empty set is a subset of any set.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem Set.eq_empty (x : Set) :
x = ∀ (y : Set), y x
Informal translation

A set $x$ is empty if and only if for all sets $y$, $y$ is not an element of $x$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected]
def Set.insert  :
Set

insert x y is the set {x} ∪ y

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[simp]
theorem Set.mem_insert {x y z : Set} :
x x = y x z
Informal translation

$x$ is an element of the set $y\cup z$ if and only if $x=y$ or $x$ is an element of $z$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Set.mem_singleton {x y : Set} :
x {y} x = y
Informal translation

$x\in\{y\}$ if and only if $x=y$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Set.mem_pair {x y z : Set} :
x {y, z} x = y x = z
Informal translation

$x$ is an element of $\{y,z\}$ if and only if $x=y$ or $x=z$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
def Set.omega  :

omega is the first infinite von Neumann ordinal

Equations
@[simp]
theorem Set.omega_zero  :
Informal translation

The empty set is a countable set.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Set.omega_succ {n : Set} :
Informal translation

If $n$ is a set, then $n\cup\{n\}$ is a set.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected]
def Set.sep (p : Set → Prop) :

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

Equations
@[protected, instance]
def Set.has_sep  :
Equations
@[simp]
theorem Set.mem_sep {p : Set → Prop} {x y : Set} :
y {y ∈ x | p y} y x p y
Informal translation

$y\in\{y\in x\mid p(y)\}$ if and only if $y\in x$ and $p(y)$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
def Set.powerset  :

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

Equations
@[simp]
theorem Set.mem_powerset {x y : Set} :
Informal translation

$y$ is a subset of $x$ if and only if $y$ is an element of the powerset of $x$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem Set.sUnion_lem {α β : Type u} (A : α → pSet) (B : β → pSet) (αβ : ∀ (a : α), ∃ (b : β), (A a).equiv (B b)) (a : (⋃₀ A).type) :
∃ (b : (⋃₀ B).type), ((⋃₀ A).func a).equiv ((⋃₀ B).func b)
Informal translation

Let $A$ and $B$ be families of sets indexed by $α$ and $β$, respectively. Suppose that for each $a\in\bigcup_{α}A$ there is a $b\in\bigcup_{β}B$ such that $A(a)$ is equinumerous to $B(b)$. Then there is a $b\in\bigcup_{β}B$ such that $A(a)$ is equinumerous to $B(b)$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
def Set.sUnion  :

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

Equations
@[simp]
theorem Set.mem_sUnion {x y : Set} :
y ⋃₀ x ∃ (z : Set) (H : z x), y z
Informal translation

$y$ is an element of the union of the sets $x$ if and only if there is a set $z$ in $x$ such that $y$ is an element of $z$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Set.sUnion_singleton {x : Set} :
⋃₀ {x} = x
Informal translation

The union of a singleton set is the set itself.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem Set.singleton_inj {x y : Set} (H : {x} = {y}) :
x = y
Informal translation

If $x$ and $y$ are sets and $\{x\}=\{y\}$, then $x=y$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected]
def Set.union (x y : Set) :

The binary union operation

Equations
@[protected]
def Set.inter (x y : Set) :

The binary intersection operation

Equations
@[protected]
def Set.diff (x y : Set) :

The set difference operation

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem Set.mem_union {x y z : Set} :
z x y z x z y
Informal translation

An element $z$ is in the union of $x$ and $y$ if and only if $z$ is in $x$ or $z$ is in $y$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Set.mem_inter {x y z : Set} :
z x y z x z y
Informal translation

$z\in x\cap y$ if and only if $z\in x$ and $z\in y$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Set.mem_diff {x y z : Set} :
z x \ y z x z y
Informal translation

$z\in x\setminus y$ if and only if $z\in x$ and $z\notin y$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem Set.induction_on {p : Set → Prop} (x : Set) (h : ∀ (x : Set), (∀ (y : Set), y xp y)p x) :
p x

Induction on the ∈ relation.

Informal translation

Let $p$ be a property of sets. Then $p$ holds for all sets.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem Set.mem_wf  :
Informal translation

The relation $x\in y$ is well-founded.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected, instance]
Equations
@[protected, instance]
theorem Set.mem_asymm {x y : Set} :
x yy x
Informal translation

If $x$ is a member of $y$, then $y$ is not a member of $x$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem Set.mem_irrefl (x : Set) :
x x
Informal translation

The set $x$ does not contain itself.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem Set.regularity (x : Set) (h : x ) :
∃ (y : Set) (H : y x), x y =
Informal translation

Let $x$ be a set. If $x$ is nonempty, then there is a set $y$ such that $y\in x$ and $x\cap y=\emptyset$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
def Set.image (f : SetSet) [H : f] :

The image of a (definable) ZFC set function

Equations
• = let r : := in , _⟩
theorem Set.image.mk (f : SetSet) [H : f] (x : Set) {y : Set} (h : y x) :
f y x
Informal translation

Let $f:X\to Y$ be a definable function. Then $f(y)\in f(X)$ for all $y\in X$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Set.mem_image {f : SetSet} [H : f] {x y : Set} :
y x ∃ (z : Set) (H : z x), f z = y
Informal translation

Let $f:X\to Y$ be a definable function. Then $y\in f(X)$ if and only if there is $x\in X$ such that $f(x)=y$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
def Set.pair (x y : Set) :

Kuratowski ordered pair

Equations
• x.pair y = {{x}, {x, y}}
Instances for Set.pair
def Set.pair_sep (p : SetSet → Prop) (x y : Set) :

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

Equations
@[simp]
theorem Set.mem_pair_sep {p : SetSet → Prop} {x y z : Set} :
z x y ∃ (a : Set) (H : a x) (b : Set) (H : b y), z = a.pair b p a b
Informal translation

$z\in\{(a,b)\mid a\in x, b\in y, p(a,b)\}$ if and only if there are $a\in x$ and $b\in y$ such that $z=(a,b)$ and $p(a,b)$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem Set.pair_inj {x y x' y' : Set} (H : x.pair y = x'.pair y') :
x = x' y = y'
Informal translation

If $x\times y=x'\times y'$, then $x=x'$ and $y=y'$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
def Set.prod  :
Set

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

Equations
@[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
Informal translation

$z$ is in the product of $x$ and $y$ if and only if there are $a\in x$ and $b\in y$ such that $z=(a,b)$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Set.pair_mem_prod {x y a b : Set} :
a.pair b x.prod y a x b y
Informal translation

$(a,b)\in X\times Y$ if and only if $a\in X$ and $b\in Y$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
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
def Set.funs (x y : Set) :

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

Equations
@[simp]
theorem Set.mem_funs {x y f : Set} :
f x.funs y x.is_func y f
Informal translation

$f$ is a function from $x$ to $y$ if and only if $f$ is an element of $x.funs y$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected, instance]
noncomputable def Set.map_definable_aux (f : SetSet) [H : f] :
(λ (y : Set), y.pair (f y))
Equations
noncomputable def Set.map (f : SetSet) [H : f] :

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

Equations
@[simp]
theorem Set.mem_map {f : SetSet} [H : f] {x y : Set} :
y x ∃ (z : Set) (H : z x), z.pair (f z) = y
Informal translation

Let $f:X\to Y$ be a definable function. Then $y\in f(x)$ if and only if there is $z\in X$ such that $f(z)=y$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem Set.map_unique {f : SetSet} [H : f] {x z : Set} (zx : z x) :
∃! (w : Set), z.pair w x
Informal translation

Let $f:X\to Y$ be a definable function. Then for each $x\in X$ there is a unique $y\in Y$ such that $f(x)=y$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Set.map_is_func {f : SetSet} [H : f] {x y : Set} :
x.is_func y (Set.map f x) ∀ (z : Set), z xf z y
Informal translation

Let $f:Set\to Set$ be a definable function. Then $x$ is a function from $y$ to $f(x)$ if and only if $f(z)\in y$ for all $z\in x$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def Class  :
Type (u_1+1)

The collection of all classes. A class is defined as a set of ZFC sets.

Equations
Instances for Class
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def Class.of_Set (x : Set) :

Coerce a ZFC set into a class

Equations
@[protected, instance]
Equations
def Class.univ  :

The universal class

Equations
def Class.to_Set (p : Set → Prop) (A : Class) :
Prop

Assert that A is a ZFC set satisfying p

Equations
@[protected]
def Class.mem (A B : Class) :
Prop

A ∈ B if A is a ZFC set which is a member of B

Equations
@[protected, instance]
Equations
theorem Class.mem_univ {A : Class} :
∃ (x : Set), x = A
Informal translation

A class $A$ is in the universe if and only if there is a set $x$ such that $A=x$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?

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

Equations
def Class.Class_to_Cong (x : Class) :

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

Equations
def Class.powerset (x : Class) :

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

Equations
def Class.sUnion (x : Class) :

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

Equations
theorem Class.of_Set.inj {x y : Set} (h : x = y) :
x = y
Informal translation

The map $x\mapsto \{x\}$ is injective.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Class.to_Set_of_Set (p : Set → Prop) (x : Set) :
p x
Informal translation

Let $p$ be a property of sets. Then $p(x)$ holds if and only if $p(\{x\})$ holds.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Class.mem_hom_left (x : Set) (A : Class) :
x A A x
Informal translation

$x\in A$ if and only if $A(x)$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Class.mem_hom_right (x y : Set) :
y x x y
Informal translation

$x\in y$ if and only if $y$ is a member of the class of all sets containing $x$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Class.subset_hom (x y : Set) :
x y x y
Informal translation

The class of $x$ is a subset of the class of $y$ if and only if $x$ is a subset of $y$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Class.sep_hom (p : Set → Prop) (x : Set) :
{y ∈ x | p y} = {y ∈ x | p y}
Informal translation

The class of all $y\in x$ such that $p(y)$ is equal to the class of all $y\in x$ such that $p(y)$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Class.empty_hom  :
Informal translation

The class of the empty set is the empty set.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Class.insert_hom (x y : Set) :
= y)
Informal translation

The class of a set $x$ with an element $y$ added is the class of the set $x$ with the element $y$ added.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Class.union_hom (x y : Set) :
x y = (x y)
Informal translation

The union of two classes is the class of the union of the two sets.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Class.inter_hom (x y : Set) :
x y = (x y)
Informal translation

The intersection of two classes is the class of the intersection of the sets.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Class.diff_hom (x y : Set) :
x \ y = (x \ y)
Informal translation

The difference of two sets is the set of elements that are in the first set but not in the second.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
Informal translation

The powerset of a set $x$ is a set.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Class.sUnion_hom (x : Set) :
Informal translation

The set of all classes of elements of a set $X$ is equal to the class of the set of all elements of $X$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
def Class.iota (p : Set → Prop) :

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

Equations
theorem Class.iota_val (p : Set → Prop) (x : Set) (H : ∀ (y : Set), p y y = x) :
= x
Informal translation

Let $p$ be a property of sets and let $x$ be a set such that $p(y)$ if and only if $y=x$. Then the class of all sets $y$ such that $p(y)$ is equal to the set $x$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem Class.iota_ex (p : Set → Prop) :

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 (Set → Prop) → Set function.

Informal translation

The class $\iota p$ is a member of the class $\mathcal{U}$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
def Class.fval (F A : Class) :

Function value

Equations
theorem Class.fval_ex (F A : Class) :
Informal translation

The class $F′A$ is a member of the class $Class.univ$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
@[simp]
theorem Set.map_fval {f : SetSet} [H : f] {x y : Set} (h : y x) :
(Set.map f x)y = (f y)
Informal translation

Let $f:Set\to Set$ be a definable function. Then for all $x,y\in Set$, $y\in x$ implies that $f(x)′y=f(y)$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
noncomputable def Set.choice (x : Set) :

A choice function on the class of nonempty ZFC sets.

Equations
theorem Set.choice_mem_aux (x : Set) (h : x) (y : Set) (yx : y x) :
classical.epsilon (λ (z : Set), z y) y
Informal translation

Let $x$ be a set such that $\emptyset\notin x$. Let $y$ be a set such that $y\in x$. Then there is a set $z$ such that $z\in y$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem Set.choice_is_func (x : Set) (h : x) :
Informal translation

Let $x$ be a set. Then the choice function $x\to \bigcup x$ is a function.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?
theorem Set.choice_mem (x : Set) (h : x) (y : Set) (yx : y x) :
Informal translation

Let $x$ be a set. If $x$ is nonempty, then there is a function $f:x\to x$ such that $f(y)\in y$ for all $y\in x$.

This translation to informal mathematics is automatically generated and should NOT be trusted! The translation is a beta feature powered by OpenAI's Codex API.
Does this translation look correct?