Documentation

MathematicalLogic.ZFSet

theorem Cardinal.IsRegular.lift {c : Cardinal.{u}} (hc : c.IsRegular) :

(Cardinal.lift.{v, u} c).IsRegular

theorem Cardinal.sum_lt_lift_of_isRegular' {ι : Type u} {f : ι → Cardinal.{v}} {c : Cardinal.{max u v}} (hc : c.IsRegular) (hι : lift.{v, u} (mk ι) < c) (hf : ∀ (i : ι), lift.{u, v} (f i) < c) :

sum f < c

theorem ZFSet.rank_mk {x : PSet.{u_1}} :

(mk x).rank = x.rank

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

Equations

x.typeSetoid = { r := fun (a b : x.Type) => x.Func a ≈ x.Func b, iseqv := ⋯ }

Instances For

def PSet.Type' (x : PSet.{u_1}) :

Type u_1

Equations

x.Type' = Quotient x.typeSetoid

Instances For

def PSet.Func' (x : PSet.{u_1}) (a : x.Type') :

Equations

x.Func' a = Quotient.liftOn a (ZFSet.mk ∘ x.Func) ⋯

Instances For

theorem PSet.func'_inj {x : PSet.{u_1}} :

Function.Injective x.Func'

theorem PSet.func'_mem_mk {x : PSet.{u_1}} (a : x.Type') :

x.Func' a ∈ ZFSet.mk x

theorem PSet.mem_mk_of_func' {x : PSet.{u_1}} (y : ZFSet.{u_1}) :

y ∈ ZFSet.mk x → ∃ (a : x.Type'), y = x.Func' a

def PSet.card (x : PSet.{u}) :

Equations

x.card = Cardinal.mk x.Type'

Instances For

theorem PSet.card_eq {x : PSet.{u}} :

Cardinal.lift.{u + 1, u} x.card = Cardinal.mk ↑(ZFSet.mk x).toSet

theorem PSet.card_congr {x y : PSet.{u}} :

x.Equiv y → x.card = y.card

def ZFSet.ofNat (n : ℕ) :

Equations

ZFSet.ofNat n = ZFSet.mk (PSet.ofNat n)

Instances For

@[simp]

theorem ZFSet.ofNat_zero :

@[simp]

theorem ZFSet.ofNat_succ {n : ℕ} :

ofNat (n + 1) = insert (ofNat n) (ofNat n)

theorem ZFSet.mem_omega_iff {x : ZFSet.{u_1}} :

x ∈ omega ↔ ∃ (n : ℕ), x = ofNat n

@[simp]

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

ZFSet.sep p x ⊆ x

def ZFSet.card :

ZFSet.{u} → Cardinal.{u}

Equations

ZFSet.card = Quotient.lift PSet.card ⋯

Instances For

theorem ZFSet.card_eq {x : ZFSet.{u}} :

Cardinal.lift.{u + 1, u} x.card = Cardinal.mk ↑x.toSet

theorem ZFSet.card_mono {x y : ZFSet.{u_1}} :

x ⊆ y → x.card ≤ y.card

theorem ZFSet.card_empty :

theorem ZFSet.card_powerset {x : ZFSet.{u_1}} :

x.powerset.card = 2 ^ x.card

theorem ZFSet.lift_card_sUnion_range_le {α : Type u} [Small.{v, u} α] {f : α → ZFSet.{v}} :

Cardinal.lift.{u, v} (range f).sUnion.card ≤ Cardinal.sum fun (i : α) => (f i).card

theorem ZFSet.rank_ofNat {n : ℕ} :

(ofNat n).rank = ↑n

theorem ZFSet.rank_omega :

omega.rank = Ordinal.omega0

theorem ZFSet.rank_image {x : ZFSet.{u}} {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] :

(image f x).rank = Ordinal.lsub fun (a : (Quotient.out x).Type') => (f ((Quotient.out x).Func' a)).rank

theorem ZFSet.card_V_lt_of_inaccessible {α : Ordinal.{u}} {κ : Cardinal.{u}} (hκ : κ.IsInaccessible) :

α < κ.ord → (vonNeumann α).card < κ

theorem ZFSet.card_lt_of_mem_V_inaccessible {x : ZFSet.{u}} {κ : Cardinal.{u}} (hκ : κ.IsInaccessible) :

x ∈ vonNeumann κ.ord → x.card < κ

theorem ZFSet.image_mem_V_of_inaccessible {f : ZFSet.{u} → ZFSet.{u}} {x : ZFSet.{u}} {κ : Cardinal.{u}} (hκ : κ.IsInaccessible) [Definable₁ f] :

x ∈ vonNeumann κ.ord → (∀ y ∈ x, f y ∈ vonNeumann κ.ord) → image f x ∈ vonNeumann κ.ord