Cardinalities of ZFC sets

In this file, we define the cardinalities of ZFC sets as ZFSet.{u} → Cardinal.{u}.

Definitions

• ZFSet.card: Cardinality of a ZFC set.

def ZFSet.card (x : ZFSet.{u}) : Cardinal.{u}

The cardinality of a ZFC set.

Equations

• x.card = Cardinal.mk (Shrink.{?u.2, ?u.2 + 1} ↥x)

theorem ZFSet.cardinalMk_coe_sort {x : ZFSet.{u}} : Cardinal.mk ↥x = Cardinal.lift.{u + 1, u} x.card

ZFSet.card x is equal to the cardinality of x as a set of ZFSets.

theorem ZFSet.card_mono {x y : ZFSet.{u}} (h : x ⊆ y) : x.card ≤ y.card

@[simp]

theorem ZFSet.card_empty : ∅.card = 0

theorem ZFSet.card_insert_le {x y : ZFSet.{u}} : (insert x y).card ≤ y.card + 1

theorem ZFSet.card_insert {x y : ZFSet.{u}} (h : x ∉ y) : (insert x y).card = y.card + 1

@[simp]

theorem ZFSet.card_singleton {x : ZFSet.{u}} : {x}.card = 1

theorem ZFSet.card_pair_of_ne {x y : ZFSet.{u}} (h : x ≠ y) : {x, y}.card = 2

theorem ZFSet.card_union_le {x y : ZFSet.{u}} : (x ∪ y).card ≤ x.card + y.card

@[simp]

theorem ZFSet.card_powerset (x : ZFSet.{u}) : x.powerset.card = 2 ^ x.card

theorem ZFSet.card_image_le {x : ZFSet.{u}} {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] : (image f x).card ≤ x.card

theorem ZFSet.lift_card_range_le {α : Type u} [Small.{v, u} α] {f : α → ZFSet.{v}} : Cardinal.lift.{u, v} (range f).card ≤ Cardinal.lift.{v, u} (Cardinal.mk α)

theorem ZFSet.iSup_card_le_card_iUnion {α : Type u} [Small.{v, u} α] {f : α → ZFSet.{v}} : ⨆ (i : α), (f i).card ≤ (iUnion fun (i : α) => f i).card

theorem ZFSet.lift_card_iUnion_le_sum_card {α : Type u} [Small.{v, u} α] {f : α → ZFSet.{v}} : Cardinal.lift.{u, v} (iUnion fun (i : α) => f i).card ≤ Cardinal.sum fun (i : α) => (f i).card