Documentation

Mathlib.SetTheory.Cardinal.ToNat

Projection from cardinal numbers to natural numbers #

In this file we define Cardinal.toNat to be the natural projection Cardinal → ℕ, sending all infinite cardinals to zero. We also prove basic lemmas about this definition.

This function sends finite cardinals to the corresponding natural, and infinite cardinals to 0.

Equations
Instances For
    @[simp]
    theorem Cardinal.toNat_toENat (a : Cardinal.{u_1}) :
    (Cardinal.toENat a).toNat = Cardinal.toNat a
    @[simp]
    theorem Cardinal.toNat_ofENat (n : ℕ∞) :
    Cardinal.toNat n = n.toNat
    @[simp]
    theorem Cardinal.toNat_natCast (n : ) :
    Cardinal.toNat n = n
    @[simp]
    theorem Cardinal.toNat_eq_zero {c : Cardinal.{u}} :
    Cardinal.toNat c = 0 c = 0 Cardinal.aleph0 c
    theorem Cardinal.toNat_ne_zero {c : Cardinal.{u}} :
    Cardinal.toNat c 0 c 0 c < Cardinal.aleph0
    @[simp]
    theorem Cardinal.toNat_pos {c : Cardinal.{u}} :
    0 < Cardinal.toNat c c 0 c < Cardinal.aleph0
    theorem Cardinal.cast_toNat_of_lt_aleph0 {c : Cardinal.{u_1}} (h : c < Cardinal.aleph0) :
    (Cardinal.toNat c) = c
    theorem Cardinal.cast_toNat_of_aleph0_le {c : Cardinal.{u_1}} (h : Cardinal.aleph0 c) :
    (Cardinal.toNat c) = 0
    theorem Cardinal.toNat_eq_iff_eq_of_lt_aleph0 {c : Cardinal.{u}} {d : Cardinal.{u}} (hc : c < Cardinal.aleph0) (hd : d < Cardinal.aleph0) :
    Cardinal.toNat c = Cardinal.toNat d c = d

    Two finite cardinals are equal iff they are equal their Cardinal.toNat projections are equal.

    theorem Cardinal.toNat_le_iff_le_of_lt_aleph0 {c : Cardinal.{u}} {d : Cardinal.{u}} (hc : c < Cardinal.aleph0) (hd : d < Cardinal.aleph0) :
    Cardinal.toNat c Cardinal.toNat d c d
    theorem Cardinal.toNat_lt_iff_lt_of_lt_aleph0 {c : Cardinal.{u}} {d : Cardinal.{u}} (hc : c < Cardinal.aleph0) (hd : d < Cardinal.aleph0) :
    Cardinal.toNat c < Cardinal.toNat d c < d
    theorem Cardinal.toNat_le_toNat {c : Cardinal.{u}} {d : Cardinal.{u}} (hcd : c d) (hd : d < Cardinal.aleph0) :
    Cardinal.toNat c Cardinal.toNat d
    @[deprecated Cardinal.toNat_le_toNat]
    theorem Cardinal.toNat_le_of_le_of_lt_aleph0 {c : Cardinal.{u}} {d : Cardinal.{u}} (hd : d < Cardinal.aleph0) (hcd : c d) :
    Cardinal.toNat c Cardinal.toNat d
    theorem Cardinal.toNat_lt_toNat {c : Cardinal.{u}} {d : Cardinal.{u}} (hcd : c < d) (hd : d < Cardinal.aleph0) :
    Cardinal.toNat c < Cardinal.toNat d
    @[deprecated Cardinal.toNat_lt_toNat]
    theorem Cardinal.toNat_lt_of_lt_of_lt_aleph0 {c : Cardinal.{u}} {d : Cardinal.{u}} (hd : d < Cardinal.aleph0) (hcd : c < d) :
    Cardinal.toNat c < Cardinal.toNat d
    @[deprecated Cardinal.toNat_natCast]
    theorem Cardinal.toNat_cast (n : ) :
    Cardinal.toNat n = n

    Alias of Cardinal.toNat_natCast.

    @[simp]
    theorem Cardinal.toNat_ofNat (n : ) [n.AtLeastTwo] :
    Cardinal.toNat (OfNat.ofNat n) = OfNat.ofNat n

    toNat has a right-inverse: coercion.

    @[simp]
    theorem Cardinal.mk_toNat_of_infinite {α : Type u} [h : Infinite α] :
    Cardinal.toNat (Cardinal.mk α) = 0
    @[simp]
    theorem Cardinal.aleph0_toNat :
    Cardinal.toNat Cardinal.aleph0 = 0
    theorem Cardinal.mk_toNat_eq_card {α : Type u} [Fintype α] :
    Cardinal.toNat (Cardinal.mk α) = Fintype.card α
    theorem Cardinal.zero_toNat :
    Cardinal.toNat 0 = 0
    theorem Cardinal.one_toNat :
    Cardinal.toNat 1 = 1
    theorem Cardinal.toNat_eq_iff {c : Cardinal.{u}} {n : } (hn : n 0) :
    Cardinal.toNat c = n c = n
    theorem Cardinal.toNat_eq_ofNat {c : Cardinal.{u}} {n : } [n.AtLeastTwo] :
    Cardinal.toNat c = OfNat.ofNat n c = OfNat.ofNat n

    A version of toNat_eq_iff for literals

    @[simp]
    theorem Cardinal.toNat_eq_one {c : Cardinal.{u}} :
    Cardinal.toNat c = 1 c = 1
    @[simp]
    theorem Cardinal.toNat_lift (c : Cardinal.{v}) :
    Cardinal.toNat (Cardinal.lift.{u, v} c) = Cardinal.toNat c
    theorem Cardinal.toNat_congr {α : Type u} {β : Type v} (e : α β) :
    Cardinal.toNat (Cardinal.mk α) = Cardinal.toNat (Cardinal.mk β)
    theorem Cardinal.toNat_mul (x : Cardinal.{u_1}) (y : Cardinal.{u_1}) :
    Cardinal.toNat (x * y) = Cardinal.toNat x * Cardinal.toNat y
    @[deprecated map_prod]
    theorem Cardinal.toNat_finset_prod {α : Type u} (s : Finset α) (f : αCardinal.{u_1}) :
    Cardinal.toNat (is, f i) = is, Cardinal.toNat (f i)
    @[simp]
    theorem Cardinal.toNat_add {c : Cardinal.{u}} {d : Cardinal.{u}} (hc : c < Cardinal.aleph0) (hd : d < Cardinal.aleph0) :
    Cardinal.toNat (c + d) = Cardinal.toNat c + Cardinal.toNat d
    @[simp]
    theorem Cardinal.toNat_lift_add_lift {a : Cardinal.{u}} {b : Cardinal.{v}} (ha : a < Cardinal.aleph0) (hb : b < Cardinal.aleph0) :
    Cardinal.toNat (Cardinal.lift.{v, u} a + Cardinal.lift.{u, v} b) = Cardinal.toNat a + Cardinal.toNat b
    @[deprecated Cardinal.toNat_lift_add_lift]
    theorem Cardinal.toNat_add_of_lt_aleph0 {a : Cardinal.{u}} {b : Cardinal.{v}} (ha : a < Cardinal.aleph0) (hb : b < Cardinal.aleph0) :
    Cardinal.toNat (Cardinal.lift.{v, u} a + Cardinal.lift.{u, v} b) = Cardinal.toNat a + Cardinal.toNat b

    Alias of Cardinal.toNat_lift_add_lift.