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
🔸 coverage
noncomputable def Cardinal.toNat :
Cardinal.{u_1} →*₀ ℕ

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

Instances For
    source
    📐 coverage
    @[simp]
    theorem Cardinal.toNat_toENat (a : Cardinal.{u_1}) :
    (toENat a).toNat = toNat a
    source
    📐 coverage
    @[simp]
    theorem Cardinal.toNat_ofENat (n : ℕ∞) :
    toNat ↑n = n.toNat
    source
    📐 coverage
    @[simp]
    theorem Cardinal.toNat_natCast (n : ℕ) :
    toNat ↑n = n
    source
    📐 coverage
    @[simp]
    theorem Cardinal.toNat_eq_zero {c : Cardinal.{u}} :
    toNat c = 0 ↔ c = 0 ∨ aleph0 ≤ c
    source
    📐 coverage
    theorem Cardinal.toNat_ne_zero {c : Cardinal.{u}} :
    toNat c ≠ 0 ↔ c ≠ 0 ∧ c < aleph0
    source
    📐 coverage
    @[simp]
    theorem Cardinal.toNat_pos {c : Cardinal.{u}} :
    0 < toNat c ↔ c ≠ 0 ∧ c < aleph0
    source
    📐 coverage
    theorem Cardinal.cast_toNat_of_lt_aleph0 {c : Cardinal.{u_1}} (h : c < aleph0) :
    ↑(toNat c) = c
    source
    📐 coverage
    theorem Cardinal.toNat_apply_of_lt_aleph0 {c : Cardinal.{u}} (h : c < aleph0) :
    toNat c = Classical.choose ⋯
    source
    📐 coverage
    theorem Cardinal.toNat_apply_of_aleph0_le {c : Cardinal.{u_1}} (h : aleph0 ≤ c) :
    toNat c = 0
    source
    📐 coverage
    theorem Cardinal.cast_toNat_of_aleph0_le {c : Cardinal.{u_1}} (h : aleph0 ≤ c) :
    ↑(toNat c) = 0
    source
    📐 coverage
    theorem Cardinal.cast_toNat_eq_iff_lt_aleph0 {c : Cardinal.{u_1}} :
    ↑(toNat c) = c ↔ c < aleph0
    source
    📐 coverage
    theorem Cardinal.toNat_strictMonoOn :
    StrictMonoOn (⇑toNat) (Set.Iio aleph0)
    source
    📐 coverage
    theorem Cardinal.toNat_monotoneOn :
    MonotoneOn (⇑toNat) (Set.Iio aleph0)
    source
    📐 coverage
    theorem Cardinal.toNat_injOn :
    Set.InjOn (⇑toNat) (Set.Iio aleph0)
    source
    📐 coverage
    theorem Cardinal.toNat_inj_of_lt_aleph0 {c d : Cardinal.{u}} (hc : c < aleph0) (hd : d < aleph0) :
    toNat c = toNat d ↔ c = d

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

    source
    📐 coverage
    theorem Cardinal.toNat_le_iff_le_of_lt_aleph0 {c d : Cardinal.{u}} (hc : c < aleph0) (hd : d < aleph0) :
    toNat c ≤ toNat d ↔ c ≤ d
    source
    📐 coverage
    theorem Cardinal.toNat_lt_iff_lt_of_lt_aleph0 {c d : Cardinal.{u}} (hc : c < aleph0) (hd : d < aleph0) :
    toNat c < toNat d ↔ c < d
    source
    📐 coverage
    theorem Cardinal.toNat_le_toNat {c d : Cardinal.{u}} (hcd : c ≤ d) (hd : d < aleph0) :
    toNat c ≤ toNat d
    source
    📐 coverage
    theorem Cardinal.toNat_lt_toNat {c d : Cardinal.{u}} (hcd : c < d) (hd : d < aleph0) :
    toNat c < toNat d
    source
    📐 coverage
    @[simp]
    theorem Cardinal.toNat_ofNat (n : ℕ) [n.AtLeastTwo] :
    toNat (OfNat.ofNat n) = OfNat.ofNat n
    source
    📐 coverage
    theorem Cardinal.toNat_rightInverse :
    Function.RightInverse Nat.cast ⇑toNat

    toNat has a right-inverse: coercion.

    source
    📐 coverage
    theorem Cardinal.toNat_surjective :
    Function.Surjective ⇑toNat
    source
    📐 coverage
    @[simp]
    theorem Cardinal.mk_toNat_of_infinite {α : Type u} [h : Infinite α] :
    toNat (mk α) = 0
    source
    📐 coverage
    @[simp]
    theorem Cardinal.aleph0_toNat :
    toNat aleph0 = 0
    source
    📐 coverage
    theorem Cardinal.mk_toNat_eq_card {α : Type u} [Fintype α] :
    toNat (mk α) = Fintype.card α
    source
    📐 coverage
    @[simp]
    theorem Cardinal.zero_toNat :
    toNat 0 = 0
    source
    📐 coverage
    theorem Cardinal.one_toNat :
    toNat 1 = 1
    source
    📐 coverage
    theorem Cardinal.toNat_eq_iff {c : Cardinal.{u}} {n : ℕ} (hn : n ≠ 0) :
    toNat c = n ↔ c = ↑n
    source
    📐 coverage
    theorem Cardinal.toNat_eq_ofNat {c : Cardinal.{u}} {n : ℕ} [n.AtLeastTwo] :
    toNat c = OfNat.ofNat n ↔ c = OfNat.ofNat n

    A version of toNat_eq_iff for literals

    source
    📐 coverage
    @[simp]
    theorem Cardinal.toNat_eq_one {c : Cardinal.{u}} :
    toNat c = 1 ↔ c = 1
    source
    📐 coverage
    theorem Cardinal.toNat_eq_one_iff_unique {α : Type u} :
    toNat (mk α) = 1 ↔ Subsingleton α ∧ Nonempty α
    source
    📐 coverage
    @[simp]
    theorem Cardinal.toNat_lift (c : Cardinal.{v}) :
    toNat (lift.{u, v} c) = toNat c
    source
    📐 coverage
    theorem Cardinal.toNat_congr {α : Type u} {β : Type v} (e : α ≃ β) :
    toNat (mk α) = toNat (mk β)
    source
    📐 coverage
    theorem Cardinal.toNat_mul (x y : Cardinal.{u_1}) :
    toNat (x * y) = toNat x * toNat y
    source
    📐 coverage
    @[simp]
    theorem Cardinal.toNat_add {c d : Cardinal.{u}} (hc : c < aleph0) (hd : d < aleph0) :
    toNat (c + d) = toNat c + toNat d
    source
    📐 coverage
    theorem Cardinal.toNat_lift_add_lift {a : Cardinal.{u}} {b : Cardinal.{v}} (ha : a < aleph0) (hb : b < aleph0) :
    toNat (lift.{v, u} a + lift.{u, v} b) = toNat a + toNat b
    source
    📐 coverage
    @[simp]
    theorem Cardinal.natCast_toNat_le (a : Cardinal.{u_1}) :
    ↑(toNat a) ≤ a
    source
    📐 coverage
    theorem Cardinal.toNat_le_iff_of_lt_aleph0 {a : Cardinal.{u}} (n : ℕ) (lt : a < aleph0) :
    toNat a ≤ n ↔ a ≤ ↑n
    source
    📐 coverage
    theorem Cardinal.toNat_eq_iff_of_lt_aleph0 {a : Cardinal.{u}} (n : ℕ) (lt : a < aleph0) :
    toNat a = n ↔ a = ↑n