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.

source
noncomputable def Cardinal.toNat :
Cardinal.{u_1} →*₀ ℕ

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

Equations
Instances For
    source
    @[simp]
    theorem Cardinal.toNat_toENat (a : Cardinal.{u_1}) :
    (Cardinal.toENat a).toNat = Cardinal.toNat a
    source
    @[simp]
    theorem Cardinal.toNat_ofENat (n : ℕ∞) :
    Cardinal.toNat ↑n = n.toNat
    source
    @[simp]
    theorem Cardinal.toNat_natCast (n : ℕ) :
    Cardinal.toNat ↑n = n
    source
    @[simp]
    theorem Cardinal.toNat_eq_zero {c : Cardinal.{u}} :
    Cardinal.toNat c = 0 ↔ c = 0 ∨ Cardinal.aleph0 ≤ c
    source
    theorem Cardinal.toNat_ne_zero {c : Cardinal.{u}} :
    Cardinal.toNat c ≠ 0 ↔ c ≠ 0 ∧ c < Cardinal.aleph0
    source
    @[simp]
    theorem Cardinal.toNat_pos {c : Cardinal.{u}} :
    0 < Cardinal.toNat c ↔ c ≠ 0 ∧ c < Cardinal.aleph0
    source
    theorem Cardinal.cast_toNat_of_lt_aleph0 {c : Cardinal.{u_1}} (h : c < Cardinal.aleph0) :
    ↑(Cardinal.toNat c) = c
    source
    theorem Cardinal.toNat_apply_of_lt_aleph0 {c : Cardinal.{u}} (h : c < Cardinal.aleph0) :
    Cardinal.toNat c = Classical.choose ⋯
    source
    theorem Cardinal.toNat_apply_of_aleph0_le {c : Cardinal.{u_1}} (h : Cardinal.aleph0 ≤ c) :
    Cardinal.toNat c = 0
    source
    theorem Cardinal.cast_toNat_of_aleph0_le {c : Cardinal.{u_1}} (h : Cardinal.aleph0 ≤ c) :
    ↑(Cardinal.toNat c) = 0
    source
    theorem Cardinal.toNat_strictMonoOn :
    StrictMonoOn (⇑Cardinal.toNat) (Set.Iio Cardinal.aleph0)
    source
    theorem Cardinal.toNat_monotoneOn :
    MonotoneOn (⇑Cardinal.toNat) (Set.Iio Cardinal.aleph0)
    source
    theorem Cardinal.toNat_injOn :
    Set.InjOn (⇑Cardinal.toNat) (Set.Iio Cardinal.aleph0)
    source
    theorem Cardinal.toNat_eq_iff_eq_of_lt_aleph0 {c 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.

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

    Alias of Cardinal.toNat_natCast.

    source
    @[simp]
    theorem Cardinal.toNat_ofNat (n : ℕ) [n.AtLeastTwo] :
    Cardinal.toNat (OfNat.ofNat n) = OfNat.ofNat n
    source
    theorem Cardinal.toNat_rightInverse :
    Function.RightInverse Nat.cast ⇑Cardinal.toNat

    toNat has a right-inverse: coercion.

    source
    theorem Cardinal.toNat_surjective :
    Function.Surjective ⇑Cardinal.toNat
    source
    @[simp]
    theorem Cardinal.mk_toNat_of_infinite {α : Type u} [h : Infinite α] :
    Cardinal.toNat (Cardinal.mk α) = 0
    source
    @[simp]
    theorem Cardinal.aleph0_toNat :
    Cardinal.toNat Cardinal.aleph0 = 0
    source
    theorem Cardinal.mk_toNat_eq_card {α : Type u} [Fintype α] :
    Cardinal.toNat (Cardinal.mk α) = Fintype.card α
    source
    @[simp]
    theorem Cardinal.zero_toNat :
    Cardinal.toNat 0 = 0
    source
    theorem Cardinal.one_toNat :
    Cardinal.toNat 1 = 1
    source
    theorem Cardinal.toNat_eq_iff {c : Cardinal.{u}} {n : ℕ} (hn : n ≠ 0) :
    Cardinal.toNat c = n ↔ c = ↑n
    source
    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

    source
    @[simp]
    theorem Cardinal.toNat_eq_one {c : Cardinal.{u}} :
    Cardinal.toNat c = 1 ↔ c = 1
    source
    theorem Cardinal.toNat_eq_one_iff_unique {α : Type u} :
    Cardinal.toNat (Cardinal.mk α) = 1 ↔ Subsingleton α ∧ Nonempty α
    source
    @[simp]
    theorem Cardinal.toNat_lift (c : Cardinal.{v}) :
    Cardinal.toNat (Cardinal.lift.{u, v} c) = Cardinal.toNat c
    source
    theorem Cardinal.toNat_congr {α : Type u} {β : Type v} (e : α ≃ β) :
    Cardinal.toNat (Cardinal.mk α) = Cardinal.toNat (Cardinal.mk β)
    source
    theorem Cardinal.toNat_mul (x y : Cardinal.{u_1}) :
    Cardinal.toNat (x * y) = Cardinal.toNat x * Cardinal.toNat y
    source
    @[deprecated map_prod]
    theorem Cardinal.toNat_finset_prod {α : Type u} (s : Finset α) (f : α → Cardinal.{u_1}) :
    Cardinal.toNat (∏ i ∈ s, f i) = ∏ i ∈ s, Cardinal.toNat (f i)
    source
    @[simp]
    theorem Cardinal.toNat_add {c d : Cardinal.{u}} (hc : c < Cardinal.aleph0) (hd : d < Cardinal.aleph0) :
    Cardinal.toNat (c + d) = Cardinal.toNat c + Cardinal.toNat d
    source
    @[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
    source
    @[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.