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}

Instances For

def PSet.Type :

PSet.{u} → Type u

The underlying type of a pre-set

Equations

Instances For

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

x.Type → PSet.{u_1}

The underlying pre-set family of a pre-set

Equations

Instances For

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

Instances For

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

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

Instances For

instance PSet.instHasSubset :

HasSubset PSet.{u_1}

Equations

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

instance PSet.instHasSSubset :

HasSSubset PSet.{u_1}

Equations

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

Instances For

instance PSet.instMembership :

Membership PSet.{u_1} PSet.{u_1}

Equations

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

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

Instances For

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

Instances For

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

def PSet.empty :

The empty pre-set

Equations

Instances For

instance PSet.instEmptyCollection :

EmptyCollection PSet.{u_1}

Equations

instance PSet.instInhabited :

Inhabited PSet.{u_1}

Equations

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

Instances For

instance PSet.instInsert :

Insert PSet.{u_1} PSet.{u_1}

Equations

instance PSet.instSingleton :

Singleton PSet.{u_1} PSet.{u_1}

Equations

instance PSet.instLawfulSingleton :

LawfulSingleton PSet.{u_1} PSet.{u_1}

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

Inhabited (insert x y).Type

Equations

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

Instances For

def PSet.omega :

The von Neumann ordinal ω

Equations

Instances For

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

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

Equations

Instances For

instance PSet.instSep :

Sep PSet.{u_1} PSet.{u_1}

Equations

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

Instances For

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

Instances For

def PSet.«term⋃₀_» :

Lean.ParserDescr

The pre-set union operator

Equations

Instances For

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

Instances For

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

Instances For

def PSet.embed :

PSet.{max (u + 1) v}

Embedding of one universe in another

Equations

Instances For

theorem PSet.lift_mem_embed (x : PSet.{u}) :

x.Lift ∈ embed