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.

Equations
    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