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.

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)

instance PSet.instPreorder : Preorder PSet.{u_1}

Equations

• PSet.instPreorder = { le := fun (x1 x2 : PSet.{?u.6}) => x1 ⊆ x2, le_refl := PSet.instPreorder._proof_2, le_trans := PSet.instPreorder._proof_3, lt_iff_le_not_le := PSet.instPreorder._proof_4 }

instance PSet.instHasSSubset : HasSSubset PSet.{u_1}

Equations

• PSet.instHasSSubset = { SSubset := fun (x1 x2 : PSet.{?u.4}) => x1 < x2 }

@[simp]

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

@[simp]

theorem PSet.lt_def (x y : PSet.{u_1}) : x < y ↔ x ⊂ y

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

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

@[deprecated PSet.notMem_of_subset (since := "2025-05-23")]

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

Alias of PSet.notMem_of_subset.

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.notMem_empty (x : PSet.{u}) : x ∉ ∅

@[deprecated PSet.notMem_empty (since := "2025-05-23")]

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

Alias of PSet.notMem_empty.

@[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.3}) => 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.3, 0} ℕ) fun (n : ULift.{?u.3, 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.76, ?u.77} α) fun (x : ULift.{?u.76, ?u.77} α) => 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.5, ?u.6 + 1} PSet.{?u.6}) fun (x : ULift.{?u.5, ?u.6 + 1} PSet.{?u.6}) => match x with | { down := x } => x.Lift

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