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}) :
ENat.toNat (Cardinal.toENat a) = Cardinal.toNat a
source
@[simp]
theorem Cardinal.toNat_ofENat (n : ℕ∞) :
Cardinal.toNat ↑n = ENat.toNat n
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_1}} (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 : 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.

source
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
source
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
source
theorem Cardinal.toNat_le_toNat {c : Cardinal.{u}} {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 : Cardinal.{u}} {d : Cardinal.{u}} (hd : d < Cardinal.aleph0) (hcd : c ≤ d) :
Cardinal.toNat c ≤ Cardinal.toNat d
source
theorem Cardinal.toNat_lt_toNat {c : Cardinal.{u}} {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 : Cardinal.{u}} {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 : ℕ) [Nat.AtLeastTwo n] :
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
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 : ℕ} [Nat.AtLeastTwo n] :
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 : Cardinal.{u_1}) (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 (Finset.prod s fun (i : α) => f i) = Finset.prod s fun (i : α) => Cardinal.toNat (f i)
source
@[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
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.