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.

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

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

Equations

• Cardinal.toNat = ENat.toNatHom.comp ↑Cardinal.toENat

@[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.toNat_apply_of_lt_aleph0 {c : Cardinal.{u}} (h : c < Cardinal.aleph0) : Cardinal.toNat c = Classical.choose ⋯

theorem Cardinal.toNat_apply_of_aleph0_le {c : Cardinal.{u_1}} (h : Cardinal.aleph0 ≤ c) : Cardinal.toNat c = 0

theorem Cardinal.cast_toNat_of_aleph0_le {c : Cardinal.{u_1}} (h : Cardinal.aleph0 ≤ c) : ↑(Cardinal.toNat c) = 0

theorem Cardinal.toNat_strictMonoOn : StrictMonoOn (⇑Cardinal.toNat) (Set.Iio Cardinal.aleph0)

theorem Cardinal.toNat_monotoneOn : MonotoneOn (⇑Cardinal.toNat) (Set.Iio Cardinal.aleph0)

theorem Cardinal.toNat_injOn : Set.InjOn (⇑Cardinal.toNat) (Set.Iio Cardinal.aleph0)

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.

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

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

theorem Cardinal.toNat_le_toNat {c 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 d : Cardinal.{u}} (hd : d < Cardinal.aleph0) (hcd : c ≤ d) : Cardinal.toNat c ≤ Cardinal.toNat d

theorem Cardinal.toNat_lt_toNat {c 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 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

theorem Cardinal.toNat_rightInverse : Function.RightInverse Nat.cast ⇑Cardinal.toNat

toNat has a right-inverse: coercion.

theorem Cardinal.toNat_surjective : Function.Surjective ⇑Cardinal.toNat

@[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 α

@[simp]

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

theorem Cardinal.toNat_eq_one_iff_unique {α : Type u} : Cardinal.toNat (Cardinal.mk α) = 1 ↔ Subsingleton α ∧ Nonempty α

@[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 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 (∏ i ∈ s, f i) = ∏ i ∈ s, Cardinal.toNat (f i)

@[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

@[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.