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.
• ZFSet: ZFC set. Defined as PSet quotiented by PSet.Equiv, the extensional equivalence.
• Class: Class. Defined as Set ZFSet.
• ZFSet.choice: Axiom of choice. Proved from Lean's axiom of choice.

Other definitions

• 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, ZFSet.omega: The von Neumann ordinal ω as a PSet, as a Set.
• Classical.allZFSetDefinable: All functions are classically definable.
• ZFSet.IsFunc : 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.
• ZFSet.funs: ZFC set of ZFC functions x → y.
• ZFSet.Hereditarily p x: Predicate that every set in the transitive closure of x has property p.
• 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".

inductive PSet : Type (u + 1)

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.

• mk (α : Type u) (A : α → PSet.{u}) : PSet.{u}

def PSet.Type : PSet.{u} → Type u

The underlying type of a pre-set

Equations

• (PSet.mk α A).Type = α

def PSet.Func (x : PSet.{u_1}) : x.Type → PSet.{u_1}

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.{u_1}) : (mk α A).Type = α

@[simp]

theorem PSet.mk_func (α : Type u_1) (A : α → PSet.{u_1}) : (mk α A).Func = A

@[simp]

theorem PSet.eta (x : PSet.{u_1}) : mk x.Type x.Func = x

def PSet.Equiv : PSet.{u_1} → PSet.{u_2} → 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

• (PSet.mk α A).Equiv (PSet.mk α_1 B) = ((∀ (a : α), ∃ (b : α_1), (A a).Equiv (B b)) ∧ ∀ (b : α_1), ∃ (a : α), (A a).Equiv (B b))

theorem PSet.equiv_iff {x : PSet.{u_1}} {y : PSet.{u_2}} : 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.{u_1}} {y : PSet.{u_2}} (h : x.Equiv y) (i : x.Type) : ∃ (j : y.Type), (x.Func i).Equiv (y.Func j)

theorem PSet.Equiv.exists_right {x : PSet.{u_1}} {y : PSet.{u_2}} (h : x.Equiv y) (j : y.Type) : ∃ (i : x.Type), (x.Func i).Equiv (y.Func j)

theorem PSet.Equiv.refl (x : PSet.{u_1}) : x.Equiv x

theorem PSet.Equiv.rfl {x : PSet.{u_1}} : x.Equiv x

theorem PSet.Equiv.euc {x : PSet.{u_1}} {y : PSet.{u_2}} {z : PSet.{u_3}} : x.Equiv y → z.Equiv y → x.Equiv z

theorem PSet.Equiv.symm {x : PSet.{u_1}} {y : PSet.{u_2}} : x.Equiv y → y.Equiv x

theorem PSet.Equiv.comm {x : PSet.{u_1}} {y : PSet.{u_2}} : x.Equiv y ↔ y.Equiv x

theorem PSet.Equiv.trans {x : PSet.{u_1}} {y : PSet.{u_2}} {z : PSet.{u_3}} (h1 : x.Equiv y) (h2 : y.Equiv z) : x.Equiv z

theorem PSet.equiv_of_isEmpty (x : PSet.{u_1}) (y : PSet.{u_2}) [IsEmpty x.Type] [IsEmpty y.Type] : x.Equiv y

instance PSet.setoid : Setoid PSet.{u_1}

Equations

• PSet.setoid = { r := PSet.Equiv, iseqv := PSet.setoid.proof_1 }

def PSet.Subset (x : PSet.{u_1}) (y : PSet.{u_2}) : 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)

instance PSet.instHasSubset : HasSubset PSet.{u_1}

Equations

• PSet.instHasSubset = { Subset := PSet.Subset }

instance PSet.instIsReflSubset : IsRefl PSet.{u_1} fun (x1 x2 : PSet.{u_1}) => x1 ⊆ x2

instance PSet.instIsTransSubset : IsTrans PSet.{u_1} fun (x1 x2 : PSet.{u_1}) => x1 ⊆ x2

theorem PSet.Equiv.ext (x y : PSet.{u_1}) : x.Equiv y ↔ x ⊆ y ∧ y ⊆ x

theorem PSet.Subset.congr_left {x y z : PSet.{u_1}} : x.Equiv y → (x ⊆ z ↔ y ⊆ z)

theorem PSet.Subset.congr_right {x y z : PSet.{u_1}} : x.Equiv y → (z ⊆ x ↔ z ⊆ y)

def PSet.Mem (y x : PSet.{u}) : Prop

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

Equations

• y.Mem x = ∃ (b : y.Type), x.Equiv (y.Func b)

instance PSet.instMembership : Membership PSet.{u_1} PSet.{u_1}

Equations

• PSet.instMembership = { mem := PSet.Mem }

theorem PSet.Mem.mk {α : Type u} (A : α → PSet.{u}) (a : α) : A a ∈ PSet.mk α A

theorem PSet.func_mem (x : PSet.{u_1}) (i : x.Type) : x.Func i ∈ x

theorem PSet.Mem.ext {x y : PSet.{u}} : (∀ (w : PSet.{u}), w ∈ x ↔ w ∈ y) → x.Equiv y

theorem PSet.Mem.congr_right {x y : PSet.{u}} : x.Equiv y → ∀ {w : PSet.{u}}, w ∈ x ↔ w ∈ y

theorem PSet.equiv_iff_mem {x y : PSet.{u}} : x.Equiv y ↔ ∀ {w : PSet.{u}}, w ∈ x ↔ w ∈ y

theorem PSet.Mem.congr_left {x y : PSet.{u}} : x.Equiv y → ∀ {w : PSet.{u}}, x ∈ w ↔ y ∈ w

theorem PSet.mem_of_subset {x y z : PSet.{u_1}} : x ⊆ y → z ∈ x → z ∈ y

theorem PSet.subset_iff {x y : PSet.{u_1}} : x ⊆ y ↔ ∀ ⦃z : PSet.{u_1}⦄, z ∈ x → z ∈ y

theorem PSet.mem_wf : WellFounded fun (x1 x2 : PSet.{u_1}) => x1 ∈ x2

instance PSet.instIsWellFoundedMem : IsWellFounded PSet.{u_1} fun (x1 x2 : PSet.{u_1}) => x1 ∈ x2

instance PSet.instWellFoundedRelation : WellFoundedRelation PSet.{u_1}

Equations

• PSet.instWellFoundedRelation = { rel := fun (x1 x2 : PSet.{?u.5}) => x1 ∈ x2, wf := PSet.mem_wf }

theorem PSet.mem_asymm {x y : PSet.{u_1}} : x ∈ y → y ∉ x

theorem PSet.mem_irrefl (x : PSet.{u_1}) : x ∉ x

theorem PSet.not_subset_of_mem {x y : PSet.{u_1}} (h : x ∈ y) : ¬y ⊆ x

theorem PSet.not_mem_of_subset {x y : PSet.{u_1}} (h : x ⊆ y) : y ∉ x

def PSet.toSet (u : PSet.{u}) : Set PSet.{u}

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

Equations

• u.toSet = {x : PSet.{?u.2} | x ∈ u}

@[simp]

theorem PSet.mem_toSet (a u : PSet.{u}) : a ∈ u.toSet ↔ a ∈ u

def PSet.Nonempty (u : PSet.{u_1}) : Prop

A nonempty set is one that contains some element.

Equations

• u.Nonempty = u.toSet.Nonempty

theorem PSet.nonempty_def (u : PSet.{u_1}) : u.Nonempty ↔ ∃ (x : PSet.{u_1}), x ∈ u

theorem PSet.nonempty_of_mem {x u : PSet.{u_1}} (h : x ∈ u) : u.Nonempty

@[simp]

theorem PSet.nonempty_toSet_iff {u : PSet.{u_1}} : u.toSet.Nonempty ↔ u.Nonempty

theorem PSet.nonempty_type_iff_nonempty {x : PSet.{u_1}} : Nonempty x.Type ↔ x.Nonempty

theorem PSet.nonempty_of_nonempty_type (x : PSet.{u_1}) [h : Nonempty x.Type] : x.Nonempty

theorem PSet.Equiv.eq {x y : PSet.{u_1}} : x.Equiv y ↔ x.toSet = y.toSet

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

instance PSet.instCoeSet : Coe PSet.{u_1} (Set PSet.{u_1})

Equations

• PSet.instCoeSet = { coe := PSet.toSet }

def PSet.empty : PSet.{u_1}

The empty pre-set

Equations

• PSet.empty = PSet.mk PEmpty.{?u.1 + 1} PEmpty.elim

instance PSet.instEmptyCollection : EmptyCollection PSet.{u_1}

Equations

• PSet.instEmptyCollection = { emptyCollection := PSet.empty }

instance PSet.instInhabited : Inhabited PSet.{u_1}

Equations

• PSet.instInhabited = { default := ∅ }

instance PSet.instIsEmptyTypeEmptyCollection : IsEmpty ∅.Type

theorem PSet.empty_def : ∅ = mk PEmpty.{u_1 + 1} PEmpty.elim

@[simp]

theorem PSet.not_mem_empty (x : PSet.{u}) : x ∉ ∅

@[simp]

theorem PSet.toSet_empty : ∅.toSet = ∅

@[simp]

theorem PSet.empty_subset (x : PSet.{u}) : ∅ ⊆ x

@[simp]

theorem PSet.not_nonempty_empty : ¬∅.Nonempty

theorem PSet.equiv_empty (x : PSet.{u_1}) [IsEmpty x.Type] : x.Equiv ∅

def PSet.insert (x y : PSet.{u_1}) : PSet.{u_1}

Insert an element into a pre-set

Equations

• x.insert y = PSet.mk (Option y.Type) fun (o : Option y.Type) => Option.casesOn o x y.Func

instance PSet.instInsert : Insert PSet.{u_1} PSet.{u_1}

Equations

• PSet.instInsert = { insert := PSet.insert }

instance PSet.instSingleton : Singleton PSet.{u_1} PSet.{u_1}

Equations

• PSet.instSingleton = { singleton := fun (s : PSet.{?u.4}) => insert s ∅ }

instance PSet.instLawfulSingleton : LawfulSingleton PSet.{u_1} PSet.{u_1}

instance PSet.instInhabitedTypeInsert (x y : PSet.{u_1}) : Inhabited (insert x y).Type

Equations

• x.instInhabitedTypeInsert y = inferInstanceAs (Inhabited (Option y.Type))

@[simp]

theorem PSet.mem_insert_iff {x y z : PSet.{u}} : x ∈ insert y z ↔ x.Equiv y ∨ x ∈ z

theorem PSet.mem_insert (x y : PSet.{u_1}) : x ∈ insert x y

theorem PSet.mem_insert_of_mem {y z : PSet.{u_1}} (x : PSet.{u_1}) (h : z ∈ y) : z ∈ insert x y

@[simp]

theorem PSet.mem_singleton {x y : PSet.{u_1}} : x ∈ {y} ↔ x.Equiv y

theorem PSet.mem_pair {x y z : PSet.{u_1}} : x ∈ {y, z} ↔ x.Equiv y ∨ x.Equiv z

def PSet.ofNat : ℕ → PSet.{u_1}

The n-th von Neumann ordinal

Equations

• PSet.ofNat 0 = ∅
• PSet.ofNat n.succ = insert (PSet.ofNat n) (PSet.ofNat n)

def PSet.omega : PSet.{u_1}

The von Neumann ordinal ω

Equations

• PSet.omega = PSet.mk (ULift.{?u.4, 0} ℕ) fun (n : ULift.{?u.4, 0} ℕ) => PSet.ofNat n.down

def PSet.sep (p : PSet.{u_1} → Prop) (x : PSet.{u_1}) : PSet.{u_1}

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

Equations

• PSet.sep p x = PSet.mk { a : x.Type // p (x.Func a) } fun (y : { a : x.Type // p (x.Func a) }) => x.Func ↑y

instance PSet.instSep : Sep PSet.{u_1} PSet.{u_1}

Equations

• PSet.instSep = { sep := PSet.sep }

theorem PSet.mem_sep {p : PSet.{u_1} → Prop} (H : ∀ (x y : PSet.{u_1}), x.Equiv y → p x → p y) {x y : PSet.{u_1}} : y ∈ PSet.sep p x ↔ y ∈ x ∧ p y

def PSet.powerset (x : PSet.{u_1}) : PSet.{u_1}

The pre-set powerset operator

Equations

• x.powerset = PSet.mk (Set x.Type) fun (p : Set x.Type) => PSet.mk { a : x.Type // p a } fun (y : { a : x.Type // p a }) => x.Func ↑y

@[simp]

theorem PSet.mem_powerset {x y : PSet.{u_1}} : y ∈ x.powerset ↔ y ⊆ x

def PSet.sUnion (a : PSet.{u_1}) : PSet.{u_1}

The pre-set union operator

Equations

• ⋃₀ a = PSet.mk ((x : a.Type) × (a.Func x).Type) fun (x : (x : a.Type) × (a.Func x).Type) => match x with | ⟨x, y⟩ => (a.Func x).Func y

def PSet.«term⋃₀_» : Lean.ParserDescr

The pre-set union operator

Equations

• PSet.«term⋃₀_» = Lean.ParserDescr.node `PSet.«term⋃₀_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋃₀ ") (Lean.ParserDescr.cat `term 110))

@[simp]

theorem PSet.mem_sUnion {x y : PSet.{u}} : y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z

@[simp]

theorem PSet.toSet_sUnion (x : PSet.{u}) : (⋃₀ x).toSet = ⋃₀ (toSet '' x.toSet)

def PSet.image (f : PSet.{u} → PSet.{u}) (x : PSet.{u}) : PSet.{u}

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.{u} → PSet.{u}} (H : ∀ (x y : PSet.{u}), x.Equiv y → (f x).Equiv (f y)) {x y : PSet.{u}} : y ∈ image f x ↔ ∃ z ∈ x, y.Equiv (f z)

def PSet.Lift : PSet.{u} → PSet.{max u v}

Universe lift operation

Equations

• (PSet.mk α A).Lift = PSet.mk (ULift.{?u.125, ?u.126} α) fun (x : ULift.{?u.125, ?u.126} α) => match x with | { down := x } => (A x).Lift

def PSet.embed : PSet.{max (u + 1) v}

Embedding of one universe in another

Equations

• PSet.embed = PSet.mk (ULift.{?u.6, ?u.7 + 1} PSet.{?u.7}) fun (x : ULift.{?u.6, ?u.7 + 1} PSet.{?u.7}) => match x with | { down := x } => x.Lift

theorem PSet.lift_mem_embed (x : PSet.{u}) : x.Lift ∈ embed

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

def PSet.Arity.Equiv {n : ℕ} : Function.OfArity PSet.{u} PSet.{u} n → Function.OfArity PSet.{u} PSet.{u} 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 = PSet.Equiv a b
• PSet.Arity.Equiv a b = ∀ (x y : PSet.{?u.612}), x.Equiv y → PSet.Arity.Equiv (a x) (b y)

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

theorem PSet.Arity.equiv_const {a : PSet.{u}} (n : ℕ) : Equiv (Function.OfArity.const PSet.{u} a n) (Function.OfArity.const PSet.{u} a n)

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

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 : Function.OfArity PSet.{?u.12} PSet.{?u.12} n // PSet.Arity.Equiv x x }

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

instance PSet.Resp.inhabited {n : ℕ} : Inhabited (Resp n)

Equations

• PSet.Resp.inhabited = { default := ⟨Function.OfArity.const PSet.{?u.13} default n, ⋯⟩ }

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

def PSet.Resp.f {n : ℕ} (f : Resp (n + 1)) (x : PSet.{u_1}) : Resp n

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

Equations

• f.f x = ⟨↑f x, ⋯⟩

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

def PSet.Resp.Equiv {n : ℕ} (a b : Resp n) : Prop

Function equivalence for functions respecting equivalence. See PSet.Arity.Equiv.

Equations

• a.Equiv b = PSet.Arity.Equiv ↑a ↑b

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

theorem PSet.Resp.Equiv.refl {n : ℕ} (a : Resp n) : a.Equiv a

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

theorem PSet.Resp.Equiv.euc {n : ℕ} {a b c : Resp n} : a.Equiv b → c.Equiv b → a.Equiv c

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

theorem PSet.Resp.Equiv.symm {n : ℕ} {a b : Resp n} : a.Equiv b → b.Equiv a

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

theorem PSet.Resp.Equiv.trans {n : ℕ} {x y z : Resp n} (h1 : x.Equiv y) (h2 : y.Equiv z) : x.Equiv z

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

instance PSet.Resp.setoid {n : ℕ} : Setoid (Resp n)

Equations

• PSet.Resp.setoid = { r := PSet.Resp.Equiv, iseqv := ⋯ }

def ZFSet : Type (u + 1)

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

Equations

• ZFSet.{?u.3} = Quotient PSet.setoid

def ZFSet.mk : PSet.{u_1} → ZFSet.{u_1}

Turns a pre-set into a ZFC set.

Equations

• ZFSet.mk = Quotient.mk''

@[simp]

theorem ZFSet.mk_eq (x : PSet.{u_1}) : ⟦x⟧ = mk x

@[simp]

theorem ZFSet.mk_out (x : ZFSet.{u_1}) : mk (Quotient.out x) = x

class ZFSet.Definable (n : ℕ) (f : (Fin n → ZFSet.{u}) → ZFSet.{u}) : Type (u + 1)

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

• out : (Fin n → PSet.{u}) → PSet.{u}

  Turns a definable function into an n-ary PSet function.

• mk_out (xs : Fin n → PSet.{u}) : ZFSet.mk (out f xs) = f fun (x : Fin n) => ZFSet.mk (xs x)

  A set function f is the image of Definable.out f.

@[reducible, inline]

abbrev ZFSet.Definable₁ (f : ZFSet.{u} → ZFSet.{u}) : Type (u + 1)

An abbrev of ZFSet.Definable for unary functions.

Equations

• ZFSet.Definable₁ f = ZFSet.Definable 1 fun (s : Fin 1 → ZFSet.{?u.18}) => f (s 0)

@[reducible, inline]

abbrev ZFSet.Definable₁.mk {f : ZFSet.{u} → ZFSet.{u}} (out : PSet.{u} → PSet.{u}) (mk_out : ∀ (x : PSet.{u}), ⟦out x⟧ = f ⟦x⟧) : Definable₁ f

A simpler constructor for ZFSet.Definable₁.

Equations

• ZFSet.Definable₁.mk out mk_out = { out := fun (xs : Fin 1 → PSet.{?u.42}) => out (xs 0), mk_out := ⋯ }

@[reducible, inline]

abbrev ZFSet.Definable₁.out (f : ZFSet.{u} → ZFSet.{u}) [Definable₁ f] : PSet.{u} → PSet.{u}

Turns a unary definable function into a unary PSet function.

Equations

• ZFSet.Definable₁.out f x = ZFSet.Definable.out (fun (s : Fin (Nat.succ 0) → ZFSet.{?u.33}) => f (s 0)) ![x]

theorem ZFSet.Definable₁.mk_out {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] {x : PSet.{u}} : ZFSet.mk (out f x) = f (ZFSet.mk x)

@[reducible, inline]

abbrev ZFSet.Definable₂ (f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}) : Type (u + 1)

An abbrev of ZFSet.Definable for binary functions.

Equations

• ZFSet.Definable₂ f = ZFSet.Definable 2 fun (s : Fin 2 → ZFSet.{?u.24}) => f (s 0) (s 1)

@[reducible, inline]

abbrev ZFSet.Definable₂.mk {f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}} (out : PSet.{u} → PSet.{u} → PSet.{u}) (mk_out : ∀ (x y : PSet.{u}), ⟦out x y⟧ = f ⟦x⟧ ⟦y⟧) : Definable₂ f

A simpler constructor for ZFSet.Definable₂.

Equations

• ZFSet.Definable₂.mk out mk_out = { out := fun (xs : Fin 2 → PSet.{?u.56}) => out (xs 0) (xs 1), mk_out := ⋯ }

@[reducible, inline]

abbrev ZFSet.Definable₂.out (f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}) [Definable₂ f] : PSet.{u} → PSet.{u} → PSet.{u}

Turns a binary definable function into a binary PSet function.

Equations

• ZFSet.Definable₂.out f x y = ZFSet.Definable.out (fun (s : Fin (Nat.succ 0).succ → ZFSet.{?u.48}) => f (s 0) (s 1)) ![x, y]

theorem ZFSet.Definable₂.mk_out {f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}} [Definable₂ f] {x y : PSet.{u}} : ZFSet.mk (out f x y) = f (ZFSet.mk x) (ZFSet.mk y)

instance ZFSet.instDefinableOfDefinable₁ (f : ZFSet.{u_1} → ZFSet.{u_1}) [Definable₁ f] (n : ℕ) (g : (Fin n → ZFSet.{u_1}) → ZFSet.{u_1}) [Definable n g] : Definable n fun (s : Fin n → ZFSet.{u_1}) => f (g s)

Equations

• ZFSet.instDefinableOfDefinable₁ f n g = { out := fun (xs : Fin n → PSet.{?u.62}) => ZFSet.Definable₁.out f (ZFSet.Definable.out g xs), mk_out := ⋯ }

instance ZFSet.instDefinableOfDefinable₂ (f : ZFSet.{u_1} → ZFSet.{u_1} → ZFSet.{u_1}) [Definable₂ f] (n : ℕ) (g₁ g₂ : (Fin n → ZFSet.{u_1}) → ZFSet.{u_1}) [Definable n g₁] [Definable n g₂] : Definable n fun (s : Fin n → ZFSet.{u_1}) => f (g₁ s) (g₂ s)

Equations

• ZFSet.instDefinableOfDefinable₂ f n g₁ g₂ = { out := fun (xs : Fin n → PSet.{?u.88}) => ZFSet.Definable₂.out f (ZFSet.Definable.out g₁ xs) (ZFSet.Definable.out g₂ xs), mk_out := ⋯ }

instance ZFSet.instDefinable (n : ℕ) (i : Fin n) : Definable n fun (s : Fin n → ZFSet.{u_1}) => s i

Equations

• ZFSet.instDefinable n i = { out := fun (s : Fin n → PSet.{?u.29}) => s i, mk_out := ⋯ }

theorem ZFSet.Definable.out_equiv {n : ℕ} (f : (Fin n → ZFSet.{u}) → ZFSet.{u}) [Definable n f] {xs ys : Fin n → PSet.{u}} (h : ∀ (i : Fin n), xs i ≈ ys i) : out f xs ≈ out f ys

theorem ZFSet.Definable₁.out_equiv (f : ZFSet.{u} → ZFSet.{u}) [Definable₁ f] {x y : PSet.{u}} (h : x ≈ y) : out f x ≈ out f y

theorem ZFSet.Definable₂.out_equiv (f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}) [Definable₂ f] {x₁ y₁ x₂ y₂ : PSet.{u}} (h₁ : x₁ ≈ y₁) (h₂ : x₂ ≈ y₂) : out f x₁ x₂ ≈ out f y₁ y₂

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

def PSet.Resp.evalAux {n : ℕ} : { f : Resp n → Function.OfArity ZFSet.{u} ZFSet.{u} n // ∀ (a b : Resp n), a.Equiv b → f a = f b }

Helper function for PSet.eval.

Equations

• PSet.Resp.evalAux = ⟨fun (a : PSet.Resp 0) => ⟦↑a⟧, PSet.Resp.evalAux.proof_4⟩
• PSet.Resp.evalAux = ⟨fun (a : PSet.Resp (n + 1)) => Quotient.lift (fun (x : PSet.{?u.359}) => ↑PSet.Resp.evalAux (a.f x)) ⋯, ⋯⟩

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

def PSet.Resp.eval (n : ℕ) : Resp n → Function.OfArity ZFSet.{u} ZFSet.{u} n

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

Equations

• PSet.Resp.eval n = ↑PSet.Resp.evalAux

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

theorem PSet.Resp.eval_val {n : ℕ} {f : Resp (n + 1)} {x : PSet.{u_1}} : eval (n + 1) f ⟦x⟧ = eval n (f.f x)

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

class inductive PSet.Definable (n : ℕ) : Function.OfArity ZFSet.{u} ZFSet.{u} n → Type (u + 1)

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.

• mk {n : ℕ} (f : PSet.Resp n) : Definable n (Resp.eval n f)

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

def PSet.Definable.EqMk {n : ℕ} (f : PSet.Resp n) {s : Function.OfArity ZFSet.{u} ZFSet.{u} n} : Resp.eval n f = s → Definable n s

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

Equations

• PSet.Definable.EqMk f ⋯ = PSet.Definable.mk f

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

def PSet.Definable.Resp {n : ℕ} (s : Function.OfArity ZFSet.{u} ZFSet.{u} n) [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

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

theorem PSet.Definable.eq {n : ℕ} (s : Function.OfArity ZFSet.{u} ZFSet.{u} n) [H : Definable n s] : Resp.eval n (Resp s) = s

@[deprecated "No deprecation message was provided." (since := "2024-09-02")]

noncomputable def Classical.allDefinable {n : ℕ} (F : Function.OfArity ZFSet.{u_1} ZFSet.{u_1} n) : PSet.Definable n F

All functions are classically definable.

Equations

• Classical.allDefinable F = PSet.Definable.EqMk ⟨Classical.choose ⋯, ⋯⟩ ⋯
• Classical.allDefinable F = PSet.Definable.EqMk ⟨fun (x : PSet.{?u.573}) => ↑(PSet.Definable.Resp (F ⟦x⟧)), ⋯⟩ ⋯

noncomputable def Classical.allZFSetDefinable {n : ℕ} (F : (Fin n → ZFSet.{u}) → ZFSet.{u}) : ZFSet.Definable n F

All functions are classically definable.

Equations

• Classical.allZFSetDefinable F = { out := fun (xs : Fin n → PSet.{?u.30}) => Quotient.out (F fun (x : Fin n) => ZFSet.mk (xs x)), mk_out := ⋯ }

theorem ZFSet.eq {x y : PSet.{u_1}} : mk x = mk y ↔ x.Equiv y

theorem ZFSet.sound {x y : PSet.{u_1}} (h : x.Equiv y) : mk x = mk y

theorem ZFSet.exact {x y : PSet.{u_1}} : mk x = mk y → x.Equiv y

@[simp, deprecated "No deprecation message was provided." (since := "2024-09-02")]

theorem ZFSet.eval_mk {n : ℕ} {f : PSet.Resp (n + 1)} {x : PSet.{u_1}} : PSet.Resp.eval (n + 1) f (mk x) = PSet.Resp.eval n (f.f x)

def ZFSet.Mem : ZFSet.{u_1} → ZFSet.{u_1} → Prop

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

Equations

• ZFSet.Mem = Quotient.lift₂ (fun (x1 x2 : PSet.{?u.17}) => x1 ∈ x2) ZFSet.Mem.proof_1

instance ZFSet.instMembership : Membership ZFSet.{u_1} ZFSet.{u_1}

Equations

• ZFSet.instMembership = { mem := fun (t s : ZFSet.{?u.5}) => s.Mem t }

@[simp]

theorem ZFSet.mk_mem_iff {x y : PSet.{u_1}} : mk x ∈ mk y ↔ x ∈ y

def ZFSet.toSet (u : ZFSet.{u}) : Set ZFSet.{u}

Convert a ZFC set into a Set of ZFC sets

Equations

• u.toSet = {x : ZFSet.{?u.2} | x ∈ u}

@[simp]

theorem ZFSet.mem_toSet (a u : ZFSet.{u}) : a ∈ u.toSet ↔ a ∈ u

instance ZFSet.small_toSet (x : ZFSet.{u}) : Small.{u, u + 1} ↑x.toSet

def ZFSet.Nonempty (u : ZFSet.{u_1}) : Prop

A nonempty set is one that contains some element.

Equations

• u.Nonempty = u.toSet.Nonempty

theorem ZFSet.nonempty_def (u : ZFSet.{u_1}) : u.Nonempty ↔ ∃ (x : ZFSet.{u_1}), x ∈ u

theorem ZFSet.nonempty_of_mem {x u : ZFSet.{u_1}} (h : x ∈ u) : u.Nonempty

@[simp]

theorem ZFSet.nonempty_toSet_iff {u : ZFSet.{u_1}} : u.toSet.Nonempty ↔ u.Nonempty

def ZFSet.Subset (x y : ZFSet.{u}) : Prop

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

Equations

• x.Subset y = ∀ ⦃z : ZFSet.{?u.19}⦄, z ∈ x → z ∈ y

instance ZFSet.hasSubset : HasSubset ZFSet.{u_1}

Equations

• ZFSet.hasSubset = { Subset := ZFSet.Subset }

theorem ZFSet.subset_def {x y : ZFSet.{u}} : x ⊆ y ↔ ∀ ⦃z : ZFSet.{u}⦄, z ∈ x → z ∈ y

instance ZFSet.instIsReflSubset : IsRefl ZFSet.{u_1} fun (x1 x2 : ZFSet.{u_1}) => x1 ⊆ x2

instance ZFSet.instIsTransSubset : IsTrans ZFSet.{u_1} fun (x1 x2 : ZFSet.{u_1}) => x1 ⊆ x2

@[simp]

theorem ZFSet.subset_iff {x y : PSet.{u_1}} : mk x ⊆ mk y ↔ x ⊆ y

@[simp]

theorem ZFSet.toSet_subset_iff {x y : ZFSet.{u_1}} : x.toSet ⊆ y.toSet ↔ x ⊆ y

theorem ZFSet.ext {x y : ZFSet.{u}} : (∀ (z : ZFSet.{u}), z ∈ x ↔ z ∈ y) → x = y

theorem ZFSet.toSet_injective : Function.Injective toSet

@[simp]

theorem ZFSet.toSet_inj {x y : ZFSet.{u_1}} : x.toSet = y.toSet ↔ x = y

instance ZFSet.instIsAntisymmSubset : IsAntisymm ZFSet.{u_1} fun (x1 x2 : ZFSet.{u_1}) => x1 ⊆ x2

def ZFSet.empty : ZFSet.{u_1}

The empty ZFC set

Equations

• ZFSet.empty = ZFSet.mk ∅

instance ZFSet.instEmptyCollection : EmptyCollection ZFSet.{u_1}

Equations

• ZFSet.instEmptyCollection = { emptyCollection := ZFSet.empty }

instance ZFSet.instInhabited : Inhabited ZFSet.{u_1}

Equations

• ZFSet.instInhabited = { default := ∅ }

@[simp]

theorem ZFSet.not_mem_empty (x : ZFSet.{u}) : x ∉ ∅

@[simp]

theorem ZFSet.toSet_empty : ∅.toSet = ∅

@[simp]

theorem ZFSet.empty_subset (x : ZFSet.{u}) : ∅ ⊆ x

@[simp]

theorem ZFSet.not_nonempty_empty : ¬∅.Nonempty

@[simp]

theorem ZFSet.nonempty_mk_iff {x : PSet.{u_1}} : (mk x).Nonempty ↔ x.Nonempty

theorem ZFSet.eq_empty (x : ZFSet.{u}) : x = ∅ ↔ ∀ (y : ZFSet.{u}), y ∉ x

theorem ZFSet.eq_empty_or_nonempty (u : ZFSet.{u_1}) : u = ∅ ∨ u.Nonempty

def ZFSet.Insert : ZFSet.{u_1} → ZFSet.{u_1} → ZFSet.{u_1}

Insert x y is the set {x} ∪ y

Equations

• ZFSet.Insert = Quotient.map₂ PSet.insert ZFSet.Insert.proof_1

instance ZFSet.instInsert : Insert ZFSet.{u_1} ZFSet.{u_1}

Equations

• ZFSet.instInsert = { insert := ZFSet.Insert }

instance ZFSet.instSingleton : Singleton ZFSet.{u_1} ZFSet.{u_1}

Equations

• ZFSet.instSingleton = { singleton := fun (x : ZFSet.{?u.4}) => insert x ∅ }

instance ZFSet.instLawfulSingleton : LawfulSingleton ZFSet.{u_1} ZFSet.{u_1}

@[simp]

theorem ZFSet.mem_insert_iff {x y z : ZFSet.{u}} : x ∈ insert y z ↔ x = y ∨ x ∈ z

theorem ZFSet.mem_insert (x y : ZFSet.{u_1}) : x ∈ insert x y

theorem ZFSet.mem_insert_of_mem {y z : ZFSet.{u_1}} (x : ZFSet.{u_1}) (h : z ∈ y) : z ∈ insert x y

@[simp]

theorem ZFSet.toSet_insert (x y : ZFSet.{u_1}) : (insert x y).toSet = insert x y.toSet

@[simp]

theorem ZFSet.mem_singleton {x y : ZFSet.{u}} : x ∈ {y} ↔ x = y

@[simp]

theorem ZFSet.toSet_singleton (x : ZFSet.{u_1}) : {x}.toSet = {x}

theorem ZFSet.insert_nonempty (u v : ZFSet.{u_1}) : (insert u v).Nonempty

theorem ZFSet.singleton_nonempty (u : ZFSet.{u_1}) : {u}.Nonempty

theorem ZFSet.mem_pair {x y z : ZFSet.{u}} : x ∈ {y, z} ↔ x = y ∨ x = z

@[simp]

theorem ZFSet.pair_eq_singleton (x : ZFSet.{u_1}) : {x, x} = {x}

@[simp]

theorem ZFSet.pair_eq_singleton_iff {x y z : ZFSet.{u_1}} : {x, y} = {z} ↔ x = z ∧ y = z

@[simp]

theorem ZFSet.singleton_eq_pair_iff {x y z : ZFSet.{u_1}} : {x} = {y, z} ↔ x = y ∧ x = z

def ZFSet.omega : ZFSet.{u_1}

omega is the first infinite von Neumann ordinal

Equations

• ZFSet.omega = ZFSet.mk PSet.omega

@[simp]

theorem ZFSet.omega_zero : ∅ ∈ omega

@[simp]

theorem ZFSet.omega_succ {n : ZFSet.{u}} : n ∈ omega → insert n n ∈ omega

def ZFSet.sep (p : ZFSet.{u_1} → Prop) : ZFSet.{u_1} → ZFSet.{u_1}

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

Equations

• ZFSet.sep p = Quotient.map (PSet.sep fun (y : PSet.{?u.17}) => p (ZFSet.mk y)) ⋯

instance ZFSet.instSep : Sep ZFSet.{u_1} ZFSet.{u_1}

Equations

• ZFSet.instSep = { sep := ZFSet.sep }

@[simp]

theorem ZFSet.mem_sep {p : ZFSet.{u} → Prop} {x y : ZFSet.{u}} : y ∈ ZFSet.sep p x ↔ y ∈ x ∧ p y

@[simp]

theorem ZFSet.sep_empty (p : ZFSet.{u_1} → Prop) : ZFSet.sep p ∅ = ∅

@[simp]

theorem ZFSet.toSet_sep (a : ZFSet.{u_1}) (p : ZFSet.{u_1} → Prop) : (ZFSet.sep p a).toSet = {x : ZFSet.{u_1} | x ∈ a.toSet ∧ p x}

def ZFSet.powerset : ZFSet.{u_1} → ZFSet.{u_1}

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

Equations

• ZFSet.powerset = Quotient.map PSet.powerset ZFSet.powerset.proof_1

@[simp]

theorem ZFSet.mem_powerset {x y : ZFSet.{u}} : y ∈ x.powerset ↔ y ⊆ x

theorem ZFSet.sUnion_lem {α β : Type u} (A : α → PSet.{u}) (B : β → PSet.{u}) (αβ : ∀ (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 ZFSet.sUnion : ZFSet.{u_1} → ZFSet.{u_1}

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

Equations

• ZFSet.sUnion = Quotient.map PSet.sUnion ZFSet.sUnion.proof_1

def ZFSet.«term⋃₀_» : Lean.ParserDescr

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

Equations

• ZFSet.«term⋃₀_» = Lean.ParserDescr.node `ZFSet.«term⋃₀_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋃₀ ") (Lean.ParserDescr.cat `term 110))

def ZFSet.sInter (x : ZFSet.{u_1}) : ZFSet.{u_1}

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

Equations

• ⋂₀ x = ZFSet.sep (fun (y : ZFSet.{?u.2}) => ∀ z ∈ x, y ∈ z) (⋃₀ x)

def ZFSet.«term⋂₀_» : Lean.ParserDescr

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

Equations

• ZFSet.«term⋂₀_» = Lean.ParserDescr.node `ZFSet.«term⋂₀_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋂₀ ") (Lean.ParserDescr.cat `term 110))

@[simp]

theorem ZFSet.mem_sUnion {x y : ZFSet.{u}} : y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z

theorem ZFSet.mem_sInter {x y : ZFSet.{u_1}} (h : x.Nonempty) : y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z

@[simp]

theorem ZFSet.sUnion_empty : ⋃₀ ∅ = ∅

@[simp]

theorem ZFSet.sInter_empty : ⋂₀ ∅ = ∅

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

theorem ZFSet.mem_sUnion_of_mem {x y z : ZFSet.{u_1}} (hy : y ∈ z) (hz : z ∈ x) : y ∈ ⋃₀ x

theorem ZFSet.not_mem_sInter_of_not_mem {x y z : ZFSet.{u_1}} (hy : y ∉ z) (hz : z ∈ x) : y ∉ ⋂₀ x

@[simp]

theorem ZFSet.sUnion_singleton {x : ZFSet.{u}} : ⋃₀ {x} = x

@[simp]

theorem ZFSet.sInter_singleton {x : ZFSet.{u}} : ⋂₀ {x} = x

@[simp]

theorem ZFSet.toSet_sUnion (x : ZFSet.{u}) : (⋃₀ x).toSet = ⋃₀ (toSet '' x.toSet)

theorem ZFSet.toSet_sInter {x : ZFSet.{u}} (h : x.Nonempty) : (⋂₀ x).toSet = ⋂₀ (toSet '' x.toSet)

theorem ZFSet.singleton_injective : Function.Injective singleton

@[simp]

theorem ZFSet.singleton_inj {x y : ZFSet.{u_1}} : {x} = {y} ↔ x = y

def ZFSet.union (x y : ZFSet.{u}) : ZFSet.{u}

The binary union operation

Equations

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

def ZFSet.inter (x y : ZFSet.{u}) : ZFSet.{u}

The binary intersection operation

Equations

• x.inter y = ZFSet.sep (fun (z : ZFSet.{?u.18}) => z ∈ y) x

def ZFSet.diff (x y : ZFSet.{u}) : ZFSet.{u}

The set difference operation

Equations

• x.diff y = ZFSet.sep (fun (z : ZFSet.{?u.18}) => z ∉ y) x

instance ZFSet.instUnion : Union ZFSet.{u_1}

Equations

• ZFSet.instUnion = { union := ZFSet.union }

instance ZFSet.instInter : Inter ZFSet.{u_1}

Equations

• ZFSet.instInter = { inter := ZFSet.inter }

instance ZFSet.instSDiff : SDiff ZFSet.{u_1}

Equations

• ZFSet.instSDiff = { sdiff := ZFSet.diff }

@[simp]

theorem ZFSet.toSet_union (x y : ZFSet.{u}) : (x ∪ y).toSet = x.toSet ∪ y.toSet

@[simp]

theorem ZFSet.toSet_inter (x y : ZFSet.{u}) : (x ∩ y).toSet = x.toSet ∩ y.toSet

@[simp]

theorem ZFSet.toSet_sdiff (x y : ZFSet.{u}) : (x \ y).toSet = x.toSet \ y.toSet

@[simp]

theorem ZFSet.mem_union {x y z : ZFSet.{u}} : z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y

@[simp]

theorem ZFSet.mem_inter {x y z : ZFSet.{u}} : z ∈ x ∩ y ↔ z ∈ x ∧ z ∈ y

@[simp]

theorem ZFSet.mem_diff {x y z : ZFSet.{u}} : z ∈ x \ y ↔ z ∈ x ∧ z ∉ y

@[simp]

theorem ZFSet.sUnion_pair {x y : ZFSet.{u}} : ⋃₀ {x, y} = x ∪ y

theorem ZFSet.mem_wf : WellFounded fun (x1 x2 : ZFSet.{u_1}) => x1 ∈ x2

theorem ZFSet.inductionOn {p : ZFSet.{u_1} → Prop} (x : ZFSet.{u_1}) (h : ∀ (x : ZFSet.{u_1}), (∀ y ∈ x, p y) → p x) : p x

Induction on the ∈ relation.

instance ZFSet.instIsWellFoundedMem : IsWellFounded ZFSet.{u_1} fun (x1 x2 : ZFSet.{u_1}) => x1 ∈ x2

instance ZFSet.instWellFoundedRelation : WellFoundedRelation ZFSet.{u_1}

Equations

• ZFSet.instWellFoundedRelation = { rel := fun (x1 x2 : ZFSet.{?u.5}) => x1 ∈ x2, wf := ZFSet.mem_wf }

theorem ZFSet.mem_asymm {x y : ZFSet.{u_1}} : x ∈ y → y ∉ x

theorem ZFSet.mem_irrefl (x : ZFSet.{u_1}) : x ∉ x

theorem ZFSet.not_subset_of_mem {x y : ZFSet.{u_1}} (h : x ∈ y) : ¬y ⊆ x

theorem ZFSet.not_mem_of_subset {x y : ZFSet.{u_1}} (h : x ⊆ y) : y ∉ x

theorem ZFSet.regularity (x : ZFSet.{u}) (h : x ≠ ∅) : ∃ y ∈ x, x ∩ y = ∅

def ZFSet.image (f : ZFSet.{u_1} → ZFSet.{u_1}) [Definable₁ f] : ZFSet.{u_1} → ZFSet.{u_1}

The image of a (definable) ZFC set function

Equations

• ZFSet.image f = Quotient.map (PSet.image (ZFSet.Definable₁.out f)) ⋯

theorem ZFSet.image.mk (f : ZFSet.{u} → ZFSet.{u}) [Definable₁ f] (x : ZFSet.{u}) {y : ZFSet.{u}} : y ∈ x → f y ∈ image f x

@[simp]

theorem ZFSet.mem_image {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] {x y : ZFSet.{u}} : y ∈ image f x ↔ ∃ z ∈ x, f z = y

@[simp]

theorem ZFSet.toSet_image (f : ZFSet.{u_1} → ZFSet.{u_1}) [Definable₁ f] (x : ZFSet.{u_1}) : (image f x).toSet = f '' x.toSet

noncomputable def ZFSet.range {α : Type u_1} [Small.{u, u_1} α] (f : α → ZFSet.{u}) : ZFSet.{u}

The range of a type-indexed family of sets.

Equations

• ZFSet.range f = ⟦PSet.mk (Shrink.{?u.30, ?u.29} α) (Quotient.out ∘ f ∘ ⇑(equivShrink α).symm)⟧

@[simp]

theorem ZFSet.mem_range {α : Type u_1} [Small.{u, u_1} α] {f : α → ZFSet.{u}} {x : ZFSet.{u}} : x ∈ range f ↔ x ∈ Set.range f

@[simp]

theorem ZFSet.toSet_range {α : Type u_1} [Small.{u, u_1} α] (f : α → ZFSet.{u}) : (range f).toSet = Set.range f

def ZFSet.pair (x y : ZFSet.{u}) : ZFSet.{u}

Kuratowski ordered pair

Equations

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

@[simp]

theorem ZFSet.toSet_pair (x y : ZFSet.{u}) : (x.pair y).toSet = {{x}, {x, y}}

def ZFSet.pairSep (p : ZFSet.{u} → ZFSet.{u} → Prop) (x y : ZFSet.{u}) : ZFSet.{u}

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

Equations

• ZFSet.pairSep p x y = ZFSet.sep (fun (z : ZFSet.{?u.29}) => ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b) (x ∪ y).powerset.powerset

@[simp]

theorem ZFSet.mem_pairSep {p : ZFSet.{u} → ZFSet.{u} → Prop} {x y z : ZFSet.{u}} : z ∈ pairSep p x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b

theorem ZFSet.pair_injective : Function.Injective2 pair

@[simp]

theorem ZFSet.pair_inj {x y x' y' : ZFSet.{u_1}} : x.pair y = x'.pair y' ↔ x = x' ∧ y = y'

def ZFSet.prod : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}

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

Equations

• ZFSet.prod = ZFSet.pairSep fun (x x : ZFSet.{?u.6}) => True

@[simp]

theorem ZFSet.mem_prod {x y z : ZFSet.{u}} : z ∈ x.prod y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b

theorem ZFSet.pair_mem_prod {x y a b : ZFSet.{u}} : a.pair b ∈ x.prod y ↔ a ∈ x ∧ b ∈ y

def ZFSet.IsFunc (x y f : ZFSet.{u}) : Prop

isFunc 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 f as a ZFC function x → y.

Equations

• x.IsFunc y f = (f ⊆ x.prod y ∧ ∀ z ∈ x, ∃! w : ZFSet.{?u.4}, z.pair w ∈ f)

def ZFSet.funs (x y : ZFSet.{u}) : ZFSet.{u}

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

Equations

• x.funs y = ZFSet.sep (x.IsFunc y) (x.prod y).powerset

@[simp]

theorem ZFSet.mem_funs {x y f : ZFSet.{u}} : f ∈ x.funs y ↔ x.IsFunc y f

instance ZFSet.instDefinable₁Singleton : Definable₁ fun (x : ZFSet.{u_1}) => {x}

Equations

• ZFSet.instDefinable₁Singleton = ZFSet.Definable₁.mk (fun (x : PSet.{?u.17}) => {x}) ZFSet.instDefinable₁Singleton.proof_1

instance ZFSet.instDefinable₂Insert : Definable₂ insert

Equations

• ZFSet.instDefinable₂Insert = ZFSet.Definable₂.mk insert ZFSet.instDefinable₂Insert.proof_1

instance ZFSet.instDefinable₂Pair : Definable₂ pair

Equations

• ZFSet.instDefinable₂Pair = id inferInstance

def ZFSet.map (f : ZFSet.{u_1} → ZFSet.{u_1}) [Definable₁ f] : ZFSet.{u_1} → ZFSet.{u_1}

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

Equations

• ZFSet.map f = ZFSet.image fun (y : ZFSet.{?u.32}) => y.pair (f y)

@[simp]

theorem ZFSet.mem_map {f : ZFSet.{u_1} → ZFSet.{u_1}} [Definable₁ f] {x y : ZFSet.{u_1}} : y ∈ map f x ↔ ∃ z ∈ x, z.pair (f z) = y

theorem ZFSet.map_unique {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] {x z : ZFSet.{u}} (zx : z ∈ x) : ∃! w : ZFSet.{u}, z.pair w ∈ map f x

@[simp]

theorem ZFSet.map_isFunc {f : ZFSet.{u_1} → ZFSet.{u_1}} [Definable₁ f] {x y : ZFSet.{u_1}} : x.IsFunc y (map f x) ↔ ∀ z ∈ x, f z ∈ y

@[irreducible]

def ZFSet.Hereditarily (p : ZFSet.{u_1} → Prop) (x : ZFSet.{u_1}) : 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

• ZFSet.Hereditarily p x = (p x ∧ ∀ y ∈ x, ZFSet.Hereditarily p y)

theorem ZFSet.hereditarily_iff {p : ZFSet.{u} → Prop} {x : ZFSet.{u}} : Hereditarily p x ↔ p x ∧ ∀ y ∈ x, Hereditarily p y

theorem ZFSet.Hereditarily.def {p : ZFSet.{u} → Prop} {x : ZFSet.{u}} : Hereditarily p x → p x ∧ ∀ y ∈ x, Hereditarily p y

Alias of the forward direction of ZFSet.hereditarily_iff.

theorem ZFSet.Hereditarily.self {p : ZFSet.{u} → Prop} {x : ZFSet.{u}} (h : Hereditarily p x) : p x

theorem ZFSet.Hereditarily.mem {p : ZFSet.{u} → Prop} {x y : ZFSet.{u}} (h : Hereditarily p x) (hy : y ∈ x) : Hereditarily p y

theorem ZFSet.Hereditarily.empty {p : ZFSet.{u} → Prop} {x : ZFSet.{u}} : Hereditarily p x → p ∅

def Class : Type (u_1 + 1)

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

Equations

• Class.{?u.3} = Set ZFSet.{?u.3}

instance instClassHasSubset : HasSubset Class.{u_1}

Equations

• instClassHasSubset = Set.instHasSubset

instance instClassEmptyCollection : EmptyCollection Class.{u_1}

Equations

• instClassEmptyCollection = Set.instEmptyCollection

instance instClassNonempty : Nonempty Class.{u_1}

Equations

• instClassNonempty = ⋯

instance instClassUnion : Union Class.{u_1}

Equations

• instClassUnion = Set.instUnion

instance instClassInter : Inter Class.{u_1}

Equations

• instClassInter = Set.instInter

instance instClassHasCompl : HasCompl Class.{u_1}

Equations

• instClassHasCompl = Set.instHasCompl

instance instClassSDiff : SDiff Class.{u_1}

Equations

• instClassSDiff = Set.instSDiff

instance instInsertZFSetClass : Insert ZFSet.{u_1} Class.{u_1}

Equations

• instInsertZFSetClass = { insert := Set.insert }

def Class.sep (p : ZFSet.{u_1} → Prop) (A : Class.{u_1}) : Class.{u_1}

{x ∈ A | p x} is the class of elements in A satisfying p

Equations

• Class.sep p A = {y : ZFSet.{?u.19} | A y ∧ p y}

theorem Class.ext {x y : Class.{u}} : (∀ (z : ZFSet.{u}), x z ↔ y z) → x = y

def Class.ofSet (x : ZFSet.{u}) : Class.{u}

Coerce a ZFC set into a class

Equations

• ↑x = {y : ZFSet.{?u.12} | y ∈ x}

instance Class.instCoeZFSet : Coe ZFSet.{u_1} Class.{u_1}

Equations

• Class.instCoeZFSet = { coe := Class.ofSet }

def Class.univ : Class.{u_1}

The universal class

Equations

• Class.univ = Set.univ

def Class.ToSet (B A : Class.{u}) : Prop

Assert that A is a ZFC set satisfying B

Equations

• B.ToSet A = ∃ (x : ZFSet.{?u.18}), ↑x = A ∧ B x

def Class.Mem (B A : Class.{u}) : Prop

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

Equations

• B.Mem A = B.ToSet A

instance Class.instMembership : Membership Class.{u_1} Class.{u_1}

Equations

• Class.instMembership = { mem := Class.Mem }

theorem Class.mem_def (A B : Class.{u}) : A ∈ B ↔ ∃ (x : ZFSet.{u}), ↑x = A ∧ B x

@[simp]

theorem Class.not_mem_empty (x : Class.{u}) : x ∉ ∅

@[simp]

theorem Class.not_empty_hom (x : ZFSet.{u}) : ¬∅ x

@[simp]

theorem Class.mem_univ {A : Class.{u}} : A ∈ univ ↔ ∃ (x : ZFSet.{u}), ↑x = A

@[simp]

theorem Class.mem_univ_hom (x : ZFSet.{u}) : univ x

theorem Class.eq_univ_iff_forall {A : Class.{u}} : A = univ ↔ ∀ (x : ZFSet.{u}), A x

theorem Class.eq_univ_of_forall {A : Class.{u}} : (∀ (x : ZFSet.{u}), A x) → A = univ

theorem Class.mem_wf : WellFounded fun (x1 x2 : Class.{u}) => x1 ∈ x2

instance Class.instIsWellFoundedMem : IsWellFounded Class.{u_1} fun (x1 x2 : Class.{u_1}) => x1 ∈ x2

instance Class.instWellFoundedRelation : WellFoundedRelation Class.{u_1}

Equations

• Class.instWellFoundedRelation = { rel := fun (x1 x2 : Class.{?u.5}) => x1 ∈ x2, wf := Class.mem_wf }

theorem Class.mem_asymm {x y : Class.{u_1}} : x ∈ y → y ∉ x

theorem Class.mem_irrefl (x : Class.{u_1}) : x ∉ x

theorem Class.univ_not_mem_univ : univ ∉ 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.congToClass (x : Set Class.{u}) : Class.{u}

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

Equations

• Class.congToClass x = {y : ZFSet.{?u.2} | ↑y ∈ x}

@[simp]

theorem Class.congToClass_empty : congToClass ∅ = ∅

def Class.classToCong (x : Class.{u}) : Set Class.{u}

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

Equations

• x.classToCong = {y : Class.{?u.2} | y ∈ x}

@[simp]

theorem Class.classToCong_empty : ∅.classToCong = ∅

def Class.powerset (x : Class.{u_1}) : Class.{u_1}

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

Equations

• x.powerset = Class.congToClass (𝒫 x)

def Class.sUnion (x : Class.{u_1}) : Class.{u_1}

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

Equations

• ⋃₀ x = ⋃₀ x.classToCong

def Class.«term⋃₀_» : Lean.ParserDescr

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

Equations

• Class.«term⋃₀_» = Lean.ParserDescr.node `Class.«term⋃₀_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋃₀ ") (Lean.ParserDescr.cat `term 110))

def Class.sInter (x : Class.{u_1}) : Class.{u_1}

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

Equations

• ⋂₀ x = ⋂₀ x.classToCong

def Class.«term⋂₀_» : Lean.ParserDescr

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

Equations

• Class.«term⋂₀_» = Lean.ParserDescr.node `Class.«term⋂₀_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋂₀ ") (Lean.ParserDescr.cat `term 110))

theorem Class.ofSet.inj {x y : ZFSet.{u}} (h : ↑x = ↑y) : x = y

@[simp]

theorem Class.toSet_of_ZFSet (A : Class.{u}) (x : ZFSet.{u}) : A.ToSet ↑x ↔ A x

@[simp]

theorem Class.coe_mem {x : ZFSet.{u}} {A : Class.{u}} : ↑x ∈ A ↔ A x

@[simp]

theorem Class.coe_apply {x y : ZFSet.{u}} : ↑y x ↔ x ∈ y

@[simp]

theorem Class.coe_subset (x y : ZFSet.{u}) : ↑x ⊆ ↑y ↔ x ⊆ y

@[simp]

theorem Class.coe_sep (p : Class.{u}) (x : ZFSet.{u}) : ↑(ZFSet.sep p x) = {y : ZFSet.{u} | y ∈ x ∧ p y}

@[simp]

theorem Class.coe_empty : ↑∅ = ∅

@[simp]

theorem Class.coe_insert (x y : ZFSet.{u}) : ↑(insert x y) = insert x ↑y

@[simp]

theorem Class.coe_union (x y : ZFSet.{u}) : ↑(x ∪ y) = ↑x ∪ ↑y

@[simp]

theorem Class.coe_inter (x y : ZFSet.{u}) : ↑(x ∩ y) = ↑x ∩ ↑y

@[simp]

theorem Class.coe_diff (x y : ZFSet.{u}) : ↑(x \ y) = ↑x \ ↑y

@[simp]

theorem Class.coe_powerset (x : ZFSet.{u}) : ↑x.powerset = (↑x).powerset

@[simp]

theorem Class.powerset_apply {A : Class.{u}} {x : ZFSet.{u}} : A.powerset x ↔ ↑x ⊆ A

@[simp]

theorem Class.sUnion_apply {x : Class.{u_1}} {y : ZFSet.{u_1}} : (⋃₀ x) y ↔ ∃ (z : ZFSet.{u_1}), x z ∧ y ∈ z

@[simp]

theorem Class.coe_sUnion (x : ZFSet.{u}) : ↑(⋃₀ x) = ⋃₀ ↑x

@[simp]

theorem Class.mem_sUnion {x y : Class.{u}} : y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z

theorem Class.sInter_apply {x : Class.{u}} {y : ZFSet.{u}} : (⋂₀ x) y ↔ ∀ (z : ZFSet.{u}), x z → y ∈ z

@[simp]

theorem Class.coe_sInter {x : ZFSet.{u}} (h : x.Nonempty) : ↑(⋂₀ x) = ⋂₀ ↑x

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

theorem Class.mem_sInter {x y : Class.{u}} (h : Set.Nonempty x) : y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z

@[simp]

theorem Class.sUnion_empty : ⋃₀ ∅ = ∅

@[simp]

theorem Class.sInter_empty : ⋂₀ ∅ = univ

theorem Class.eq_univ_of_powerset_subset {A : Class.{u_1}} (hA : A.powerset ⊆ A) : A = 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.{u_1}) : Class.{u_1}

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

Equations

• A.iota = ⋃₀ {x : ZFSet.{?u.13} | ∀ (y : ZFSet.{?u.13}), A y ↔ y = x}

theorem Class.iota_val (A : Class.{u_1}) (x : ZFSet.{u_1}) (H : ∀ (y : ZFSet.{u_1}), A y ↔ y = x) : A.iota = ↑x

theorem Class.iota_ex (A : Class.{u}) : A.iota ∈ 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.{u}) : Class.{u}

Function value

Equations

• F ′ A = Class.iota fun (y : ZFSet.{?u.19}) => Class.ToSet (fun (x : ZFSet.{?u.19}) => F (x.pair y)) A

def Class.«term_′_» : Lean.TrailingParserDescr

Function value

Equations

• Class.«term_′_» = Lean.ParserDescr.trailingNode `Class.«term_′_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ′ ") (Lean.ParserDescr.cat `term 101))

theorem Class.fval_ex (F A : Class.{u}) : F ′ A ∈ univ

@[simp]

theorem ZFSet.map_fval {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] {x y : ZFSet.{u}} (h : y ∈ x) : ↑(map f x) ′ ↑y = ↑(f y)

noncomputable def ZFSet.choice (x : ZFSet.{u}) : ZFSet.{u}

A choice function on the class of nonempty ZFC sets.

Equations

• x.choice = ZFSet.map (fun (y : ZFSet.{?u.15}) => Classical.epsilon fun (z : ZFSet.{?u.15}) => z ∈ y) x

theorem ZFSet.choice_mem_aux (x : ZFSet.{u}) (h : ∅ ∉ x) (y : ZFSet.{u}) (yx : y ∈ x) : (Classical.epsilon fun (z : ZFSet.{u}) => z ∈ y) ∈ y

theorem ZFSet.choice_isFunc (x : ZFSet.{u}) (h : ∅ ∉ x) : x.IsFunc (⋃₀ x) x.choice

theorem ZFSet.choice_mem (x : ZFSet.{u}) (h : ∅ ∉ x) (y : ZFSet.{u}) (yx : y ∈ x) : ↑x.choice ′ ↑y ∈ ↑y

noncomputable def ZFSet.toSet_equiv : ZFSet.{u} ≃ { s : Set ZFSet.{u} // Small.{u, u + 1} ↑s }

ZFSet.toSet as an equivalence.

Equations

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

@[simp]

theorem ZFSet.toSet_equiv_apply_coe (x : ZFSet.{u}) : ↑(toSet_equiv x) = x.toSet