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

Alias of Cardinal.toNat_inj_of_lt_aleph0.

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 < aleph0) (hd : d < aleph0) :
toNat c ≤ toNat d ↔ c ≤ d
source
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
theorem Cardinal.toNat_le_toNat {c d : Cardinal.{u}} (hcd : c ≤ d) (hd : d < aleph0) :
toNat c ≤ toNat d
source
theorem Cardinal.toNat_lt_toNat {c d : Cardinal.{u}} (hcd : c < d) (hd : d < aleph0) :
toNat c < toNat d
source
@[simp]
theorem Cardinal.toNat_ofNat (n : ℕ) [n.AtLeastTwo] :
toNat (OfNat.ofNat n) = OfNat.ofNat n
source
theorem Cardinal.toNat_rightInverse :
Function.RightInverse Nat.cast ⇑toNat

toNat has a right-inverse: coercion.

source
theorem Cardinal.toNat_surjective :
Function.Surjective ⇑toNat
source
@[simp]
theorem Cardinal.mk_toNat_of_infinite {α : Type u} [h : Infinite α] :
toNat (mk α) = 0
source
@[simp]
theorem Cardinal.aleph0_toNat :
toNat aleph0 = 0
source
theorem Cardinal.mk_toNat_eq_card {α : Type u} [Fintype α] :
toNat (mk α) = Fintype.card α
source
@[simp]
theorem Cardinal.zero_toNat :
toNat 0 = 0
source
theorem Cardinal.one_toNat :
toNat 1 = 1
source
theorem Cardinal.toNat_eq_iff {c : Cardinal.{u}} {n : ℕ} (hn : n ≠ 0) :
toNat c = n ↔ c = ↑n
source
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
@[simp]
theorem Cardinal.toNat_eq_one {c : Cardinal.{u}} :
toNat c = 1 ↔ c = 1
source
theorem Cardinal.toNat_eq_one_iff_unique {α : Type u} :
toNat (mk α) = 1 ↔ Subsingleton α ∧ Nonempty α
source
@[simp]
theorem Cardinal.toNat_lift (c : Cardinal.{v}) :
toNat (lift.{u, v} c) = toNat c
source
theorem Cardinal.toNat_congr {α : Type u} {β : Type v} (e : α ≃ β) :
toNat (mk α) = toNat (mk β)
source
theorem Cardinal.toNat_mul (x y : Cardinal.{u_1}) :
toNat (x * y) = toNat x * toNat y
source
@[simp]
theorem Cardinal.toNat_add {c d : Cardinal.{u}} (hc : c < aleph0) (hd : d < aleph0) :
toNat (c + d) = toNat c + toNat d
source
@[simp]
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