A model of ZFC

In this file, we model Zermelo-Fraenkel set theory (+ choice) using Lean's underlying type theory, building on the pre-sets defined in Mathlib/SetTheory/ZFC/PSet.lean.

The theory of classes is developed in Mathlib/SetTheory/ZFC/Class.lean.

Main definitions

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

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".

def ZFSet : Type (u + 1)

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

Equations

• ZFSet.{?u.1} = 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.1}) => 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.1}) => 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.1}) => 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.1}) => 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.1}) => 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.1}) => 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_reducible]

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.1}) => ZFSet.Definable₁.out f (ZFSet.Definable.out g xs), mk_out := ⋯ }

@[instance_reducible]

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.1}) => ZFSet.Definable₂.out f (ZFSet.Definable.out g₁ xs) (ZFSet.Definable.out g₂ xs), mk_out := ⋯ }

@[instance_reducible]

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.1}) => 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₂

@[instance_reducible]

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.1}) => 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

def ZFSet.toSet (x : ZFSet.{u_1}) : Set ZFSet.{u_1}

Convert a ZFC set into a Set of ZFC sets

Equations

• x.toSet = {y : ZFSet.{?u.1} | Quotient.lift₂ (fun (x1 x2 : PSet.{?u.1}) => x1 ∈ x2) ZFSet.toSet._proof_1 y x}

@[instance_reducible]

instance ZFSet.instSetLike : SetLike ZFSet.{u} ZFSet.{u}

Equations

• ZFSet.instSetLike = { coe := ZFSet.toSet, coe_injective := ⋯ }

@[deprecated "use `∈` notation" (since := "2026-03-16")]

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

• x1✝.Mem x2✝ = (x1✝ ∈ x2✝)

@[simp]

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

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

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

@[instance_reducible]

instance ZFSet.instPartialOrder : PartialOrder ZFSet.{u}

Equations

• ZFSet.instPartialOrder = PartialOrder.ofSetLike ZFSet.{?u.1} ZFSet.{?u.1}

instance ZFSet.small_coe (x : ZFSet.{u}) : Small.{u, u + 1} ↥x

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

A nonempty set is one that contains some element.

Equations

• u.Nonempty = (↑u).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_coe {x : ZFSet.{u}} : (↑x).Nonempty ↔ x.Nonempty

@[deprecated "This is now a syntactic equality" (since := "2026-03-18")]

theorem ZFSet.le_def {x y : ZFSet.{u}} : x ⊆ y ↔ x ⊆ y

@[deprecated "This is now a syntactic equality" (since := "2026-03-18")]

theorem ZFSet.lt_def {x y : ZFSet.{u}} : x ⊂ y ↔ x ⊂ y

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

instance ZFSet.instReflLe : Std.Refl fun (x1 x2 : ZFSet.{u_1}) => x1 ⊆ x2

instance ZFSet.instIsTransLe : 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

theorem ZFSet.coe_subset_coe {x y : ZFSet.{u}} : ↑x ⊆ ↑y ↔ x ⊆ y

instance ZFSet.instAntisymmLe : Std.Antisymm fun (x1 x2 : ZFSet.{u_1}) => x1 ⊆ x2

instance ZFSet.instIsNonstrictStrictOrderLeLt : IsNonstrictStrictOrder ZFSet.{u_1} (fun (x1 x2 : ZFSet.{u_1}) => x1 ⊆ x2) fun (x1 x2 : ZFSet.{u_1}) => x1 ⊂ x2

def ZFSet.empty : ZFSet.{u_1}

The empty ZFC set

Equations

• ZFSet.empty = ZFSet.mk ∅

@[instance_reducible]

instance ZFSet.instEmptyCollection : EmptyCollection ZFSet.{u_1}

Equations

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

@[instance_reducible]

instance ZFSet.instInhabited : Inhabited ZFSet.{u_1}

Equations

• ZFSet.instInhabited = { default := ∅ }

@[simp]

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

@[simp]

theorem ZFSet.coe_empty : ↑∅ = ∅

@[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_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• ZFSet.instSingleton = { singleton := fun (x : ZFSet.{?u.1}) => 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.coe_insert (x y : ZFSet.{u_1}) : ↑(insert x y) = insert x ↑y

@[simp]

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

theorem ZFSet.notMem_singleton {x y : ZFSet.{u}} : x ∉ {y} ↔ x ≠ y

@[simp]

theorem ZFSet.coe_singleton (x : ZFSet.{u_1}) : ↑{x} = {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.1}) => p (ZFSet.mk y)) ⋯

@[instance_reducible]

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 ∅ = ∅

theorem ZFSet.sep_subset {x : ZFSet.{u_1}} {p : ZFSet.{u_1} → Prop} : ZFSet.sep p x ⊆ x

@[simp]

theorem ZFSet.coe_sep (a : ZFSet.{u_1}) (p : ZFSet.{u_1} → Prop) : ↑(ZFSet.sep p a) = {x : ZFSet.{u_1} | x ∈ a ∧ 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. Uses ⋃₀ notation, scoped under the ZFSet namespace.

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. Uses ⋃₀ notation, scoped under the ZFSet namespace.

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 ⋂₀ ∅ = ∅. Uses ⋂₀ notation, scoped under the ZFSet namespace.

Equations

• x.sInter = ZFSet.sep (fun (y : ZFSet.{?u.1}) => ∀ z ∈ x, y ∈ z) x.sUnion

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

The intersection operator, the collection of elements in all of the elements of a ZFC set. We define ⋂₀ ∅ = ∅. Uses ⋂₀ notation, scoped under the ZFSet namespace.

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.sUnion ↔ ∃ z ∈ x, y ∈ z

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

@[simp]

theorem ZFSet.sUnion_empty : ∅.sUnion = ∅

@[simp]

theorem ZFSet.sInter_empty : ∅.sInter = ∅

theorem ZFSet.mem_of_mem_sInter {x y z : ZFSet.{u_1}} (hy : y ∈ x.sInter) (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.sUnion

theorem ZFSet.notMem_sInter_of_notMem {x y z : ZFSet.{u_1}} (hy : y ∉ z) (hz : z ∈ x) : y ∉ x.sInter

@[simp]

theorem ZFSet.sUnion_singleton {x : ZFSet.{u}} : {x}.sUnion = x

@[simp]

theorem ZFSet.sInter_singleton {x : ZFSet.{u}} : {x}.sInter = x

@[simp]

theorem ZFSet.coe_sUnion (x : ZFSet.{u}) : ↑x.sUnion = ⋃₀ (SetLike.coe '' ↑x)

@[simp]

theorem ZFSet.coe_sInter {x : ZFSet.{u}} (h : x.Nonempty) : ↑x.sInter = ⋂₀ (SetLike.coe '' ↑x)

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}.sUnion

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

The binary intersection operation

Equations

• x.inter y = ZFSet.sep (fun (z : ZFSet.{?u.1}) => 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.1}) => z ∉ y) x

@[instance_reducible]

instance ZFSet.instUnion : Union ZFSet.{u_1}

Equations

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

@[instance_reducible]

instance ZFSet.instInter : Inter ZFSet.{u_1}

Equations

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

@[instance_reducible]

instance ZFSet.instSDiff : SDiff ZFSet.{u_1}

Equations

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

@[simp]

theorem ZFSet.sUnion_pair (x y : ZFSet.{u}) : {x, y}.sUnion = x ∪ y

@[simp]

theorem ZFSet.sep_mem (x y : ZFSet.{u}) : ZFSet.sep (fun (x : ZFSet.{u}) => x ∈ y) x = x ∩ y

@[simp]

theorem ZFSet.sep_notMem (x y : ZFSet.{u}) : ZFSet.sep (fun (x : ZFSet.{u}) => x ∉ y) x = x \ y

@[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_sdiff {x y z : ZFSet.{u}} : z ∈ x \ y ↔ z ∈ x ∧ z ∉ y

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem ZFSet.inter_eq_left_of_subset {x y : ZFSet.{u}} (hxy : x ⊆ y) : x ∩ y = x

@[simp]

theorem ZFSet.inter_eq_right_of_subset {x y : ZFSet.{u}} (hyx : y ⊆ x) : x ∩ y = y

def ZFSet.powersetEquiv (x : ZFSet.{u}) : ↥x.powerset ≃ ↑(𝒫 ↑x)

ZFSet.powerset is equivalent to Set.powerset.

Equations

• x.powersetEquiv = { toFun := fun (y : ↥x.powerset) => ⟨↑↑y, ⋯⟩, invFun := fun (s : ↑(𝒫 ↑x)) => ⟨ZFSet.sep (fun (x_1 : ZFSet.{?u.1}) => x_1 ∈ ↑s) x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem ZFSet.insert_eq (x y : ZFSet.{u_1}) : insert 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_reducible]

instance ZFSet.instWellFoundedRelation : WellFoundedRelation ZFSet.{u_1}

Equations

• ZFSet.instWellFoundedRelation = { rel := fun (x1 x2 : ZFSet.{?u.1}) => 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.notMem_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.coe_image (f : ZFSet.{u_1} → ZFSet.{u_1}) [Definable₁ f] (x : ZFSet.{u_1}) : ↑(image f x) = f '' ↑x

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.2, ?u.1} α) (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 ↔ ∃ (i : α), f i = x

@[simp]

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

theorem ZFSet.mem_range_self {α : Type u_1} [Small.{u, u_1} α] {f : α → ZFSet.{u}} (a : α) : f a ∈ range f

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

Indexed union of a family of ZFC sets. Uses ⋃ notation, scoped under the ZFSet namespace.

Equations

• ZFSet.iUnion f = (ZFSet.range f).sUnion

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

Indexed union of a family of ZFC sets. Uses ⋃ notation, scoped under the ZFSet namespace.

Equations

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

@[simp]

theorem ZFSet.mem_iUnion {α : Type u_1} [Small.{u, u_1} α] {f : α → ZFSet.{u}} {x : ZFSet.{u}} : (x ∈ iUnion fun (i : α) => f i) ↔ ∃ (i : α), x ∈ f i

@[simp]

theorem ZFSet.coe_iUnion {α : Type u_1} [Small.{u, u_1} α] (f : α → ZFSet.{u}) : ↑(iUnion fun (i : α) => f i) = ⋃ (i : α), ↑(f i)

theorem ZFSet.subset_iUnion {α : Type u_1} [Small.{u, u_1} α] (f : α → ZFSet.{u}) (i : α) : f i ⊆ iUnion fun (i : α) => f i

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

Kuratowski ordered pair

Equations

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

@[simp]

theorem ZFSet.coe_pair (x y : ZFSet.{u}) : ↑(x.pair y) = {{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.1}) => ∃ 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_1 : ZFSet.{?u.1}) => 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.1}, 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_reducible]

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

Equations

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

@[instance_reducible]

instance ZFSet.instDefinable₂Insert : Definable₂ insert

Equations

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

@[instance_reducible]

instance ZFSet.instDefinable₂Pair : Definable₂ pair

Equations

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

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.1}) => 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 ∅