Projection from cardinal numbers to PartENat

In this file we define the projection Cardinal.toPartENat and prove basic properties of this projection.

noncomputable def Cardinal.toPartENat : Cardinal.{u_1} →+o PartENat

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Cardinal.partENatOfENat_toENat (c : Cardinal.{u_1}) : ↑(toENat c) = toPartENat c

@[simp]

theorem Cardinal.toPartENat_natCast (n : ℕ) : toPartENat ↑n = ↑n

theorem Cardinal.toPartENat_apply_of_lt_aleph0 {c : Cardinal.{u_1}} (h : c < aleph0) : toPartENat c = ↑(toNat c)

theorem Cardinal.toPartENat_eq_top {c : Cardinal.{u_1}} : toPartENat c = ⊤ ↔ aleph0 ≤ c

theorem Cardinal.toPartENat_apply_of_aleph0_le {c : Cardinal.{u_1}} (h : aleph0 ≤ c) : toPartENat c = ⊤

@[simp]

theorem Cardinal.mk_toPartENat_of_infinite {α : Type u} [h : Infinite α] : toPartENat (mk α) = ⊤

@[simp]

theorem Cardinal.aleph0_toPartENat : toPartENat aleph0 = ⊤

theorem Cardinal.toPartENat_surjective : Function.Surjective ⇑toPartENat

theorem Cardinal.toPartENat_strictMonoOn : StrictMonoOn (⇑toPartENat) (Set.Iic aleph0)

theorem Cardinal.toPartENat_le_iff_of_le_aleph0 {c c' : Cardinal.{u_1}} (h : c ≤ aleph0) : toPartENat c ≤ toPartENat c' ↔ c ≤ c'

theorem Cardinal.toPartENat_le_iff_of_lt_aleph0 {c c' : Cardinal.{u_1}} (hc' : c' < aleph0) : toPartENat c ≤ toPartENat c' ↔ c ≤ c'

theorem Cardinal.toPartENat_inj_of_le_aleph0 {c c' : Cardinal.{u_1}} (hc : c ≤ aleph0) (hc' : c' ≤ aleph0) : toPartENat c = toPartENat c' ↔ c = c'

@[deprecated Cardinal.toPartENat_inj_of_le_aleph0 (since := "2024-12-29")]

theorem Cardinal.toPartENat_eq_iff_of_le_aleph0 {c c' : Cardinal.{u_1}} (hc : c ≤ aleph0) (hc' : c' ≤ aleph0) : toPartENat c = toPartENat c' ↔ c = c'

Alias of Cardinal.toPartENat_inj_of_le_aleph0.

theorem Cardinal.toPartENat_mono {c c' : Cardinal.{u_1}} (h : c ≤ c') : toPartENat c ≤ toPartENat c'

theorem Cardinal.toPartENat_lift (c : Cardinal.{v}) : toPartENat (lift.{u, v} c) = toPartENat c

theorem Cardinal.toPartENat_congr {α : Type u} {β : Type v} (e : α ≃ β) : toPartENat (mk α) = toPartENat (mk β)

theorem Cardinal.mk_toPartENat_eq_coe_card {α : Type u} [Fintype α] : toPartENat (mk α) = ↑(Fintype.card α)