Documentation

Mathlib.SetTheory.ZFC.Cardinal

Cardinalities of ZFC sets #

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

Definitions #

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

The cardinality of a ZFC set.

Instances For
    source
    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.

    source
    theorem ZFSet.card_mono {x y : ZFSet.{u}} (h : x ⊆ y) :
    x.card ≤ y.card
    source
    @[simp]
    theorem ZFSet.card_empty :
    ∅.card = 0
    source
    theorem ZFSet.card_insert_le {x y : ZFSet.{u}} :
    (insert x y).card ≤ y.card + 1
    source
    theorem ZFSet.card_insert {x y : ZFSet.{u}} (h : x ∉ y) :
    (insert x y).card = y.card + 1
    source
    @[simp]
    theorem ZFSet.card_singleton {x : ZFSet.{u}} :
    {x}.card = 1
    source
    theorem ZFSet.card_pair_of_ne {x y : ZFSet.{u}} (h : x ≠ y) :
    {x, y}.card = 2
    source
    theorem ZFSet.card_union_le {x y : ZFSet.{u}} :
    (x ∪ y).card ≤ x.card + y.card
    source
    @[simp]
    theorem ZFSet.card_powerset (x : ZFSet.{u}) :
    x.powerset.card = 2 ^ x.card
    source
    theorem ZFSet.card_image_le {x : ZFSet.{u}} {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] :
    (image f x).card ≤ x.card
    source
    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 α)
    source
    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
    source
    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