Pre-sets

A pre-set is inductively defined by its indexing type and its members, which are themselves pre-sets.

After defining pre-sets we define extensional equality over them, also inductively. We construct a Setoid instance from it, and in Mathlib/SetTheory/ZFC/Basic.lean we define ZFC sets as the quotient of pre-sets by extensional equality.

Main definitions

• PSet: Pre-set.
• 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: The von Neumann ordinal ω as a PSet.

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

• Type : Type u

  The underlying type of a pre-set

• Func : self.Type → PSet.{u}

  The underlying pre-set family of a pre-set

@[deprecated "This now holds by reducible defeq for structure projection." (since := "2026-09-20")]

theorem PSet.mk_type (α : Type u_1) (A : α → PSet.{u_1}) : { «Type» := α, Func := A }.Type = α

@[deprecated "This now holds by reducible defeq for structure projection." (since := "2026-09-20")]

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

theorem PSet.eta (x : PSet.{u_1}) : { «Type» := x.Type, Func := 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

• { «Type» := «Type», Func := A }.Equiv { «Type» := Type_1, Func := B } = ((∀ (a : «Type»), ∃ (b : Type_1), (A a).Equiv (B b)) ∧ ∀ (b : Type_1), ∃ (a : «Type»), (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_reducible]

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

instance PSet.instLE : LE PSet.{u_1}

Equations

• PSet.instLE = { le := PSet.Subset }

@[instance_reducible]

instance PSet.instPreorder : Preorder PSet.{u_1}

Equations

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

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)

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

theorem PSet.le_def (x y : PSet.{u_1}) : x ⊆ y ↔ x ⊆ y

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

theorem PSet.lt_def (x y : PSet.{u_1}) : x ⊂ y ↔ x ⊂ 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_reducible]

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

Equations

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

theorem PSet.mem_def {x y : PSet.{u_1}} : x ∈ y ↔ ∃ (b : y.Type), x.Equiv (y.Func b)

theorem PSet.Mem.mk {α : Type u} (A : α → PSet.{u}) (a : α) : A a ∈ { «Type» := α, Func := 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

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

@[instance_reducible]

instance PSet.instWellFoundedRelation : WellFoundedRelation PSet.{u_1}

Equations

• PSet.instWellFoundedRelation = { rel := fun (x1 x2 : PSet.{?u.1}) => 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.notMem_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.1} | 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_reducible]

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 = { «Type» := PEmpty.{?u.1 + 1}, Func := PEmpty.elim }

@[instance_reducible]

instance PSet.instEmptyCollection : EmptyCollection PSet.{u_1}

Equations

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

@[instance_reducible]

instance PSet.instInhabited : Inhabited PSet.{u_1}

Equations

• PSet.instInhabited = { default := ∅ }

instance PSet.instIsEmptyTypeEmptyCollection : IsEmpty ∅.Type

theorem PSet.empty_def : ∅ = { «Type» := PEmpty.{u_1 + 1}, Func := PEmpty.elim }

@[simp]

theorem PSet.notMem_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 = { «Type» := Option y.Type, Func := fun (o : Option y.Type) => Option.casesOn o x y.Func }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

@[instance_reducible]

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

Equations

• x.instInhabitedTypeInsert y = { default := PSet.instInhabitedTypeInsert._aux_1 x y }

@[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 = { «Type» := ULift.{?u.1, 0} ℕ, Func := fun (n : ULift.{?u.1, 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 = { «Type» := { a : x.Type // p (x.Func a) }, Func := fun (y : { a : x.Type // p (x.Func a) }) => x.Func ↑y }

@[instance_reducible]

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 = { «Type» := Set x.Type, Func := fun (p : Set x.Type) => { «Type» := ↑p, Func := fun (y : ↑p) => 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 = { «Type» := (x : a.Type) × (a.Func x).Type, Func := 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 : PSet.{u}), 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 = { «Type» := x.Type, Func := 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 : PSet.{u}), z ∈ x ∧ y.Equiv (f z)

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

Universe lift operation

Equations

• { «Type» := α, Func := A }.Lift = { «Type» := ULift.{?u.1, ?u.2} α, Func := fun (x : ULift.{?u.1, ?u.2} α) => 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 = { «Type» := ULift.{?u.1, ?u.2 + 1} PSet.{?u.2}, Func := fun (x : ULift.{?u.1, ?u.2 + 1} PSet.{?u.2}) => match x with | { down := x } => x.Lift }

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