Documentation

Mathlib.SetTheory.ZFC.PSet

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}) :

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

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) :

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

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}) :

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}) :

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) :

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}) :

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}) :

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) :

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

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 :

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}) :

@[simp]

theorem PSet.not_nonempty_empty :

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

def PSet.insert (x y : 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 :

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}) :

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}) :

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}) :

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}) :

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