Documentation

Mathlib.Deprecated.Cardinal.PartENat

Projection from cardinal numbers to PartENat #

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

source
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.
Instances For
    source
    @[simp]
    theorem Cardinal.partENatOfENat_toENat (c : Cardinal.{u_1}) :
    ↑(toENat c) = toPartENat c
    source
    @[simp]
    theorem Cardinal.toPartENat_natCast (n : ℕ) :
    toPartENat ↑n = ↑n
    source
    theorem Cardinal.toPartENat_apply_of_lt_aleph0 {c : Cardinal.{u_1}} (h : c < aleph0) :
    toPartENat c = ↑(toNat c)
    source
    theorem Cardinal.toPartENat_eq_top {c : Cardinal.{u_1}} :
    toPartENat c = ⊤ ↔ aleph0 ≤ c
    source
    theorem Cardinal.toPartENat_apply_of_aleph0_le {c : Cardinal.{u_1}} (h : aleph0 ≤ c) :
    toPartENat c = ⊤
    source
    @[simp]
    theorem Cardinal.mk_toPartENat_of_infinite {α : Type u} [h : Infinite α] :
    toPartENat (mk α) = ⊤
    source
    @[simp]
    theorem Cardinal.aleph0_toPartENat :
    toPartENat aleph0 = ⊤
    source
    theorem Cardinal.toPartENat_surjective :
    Function.Surjective ⇑toPartENat
    source
    theorem Cardinal.toPartENat_strictMonoOn :
    StrictMonoOn (⇑toPartENat) (Set.Iic aleph0)
    source
    theorem Cardinal.toPartENat_le_iff_of_le_aleph0 {c c' : Cardinal.{u_1}} (h : c ≤ aleph0) :
    toPartENat c ≤ toPartENat c' ↔ c ≤ c'
    source
    theorem Cardinal.toPartENat_le_iff_of_lt_aleph0 {c c' : Cardinal.{u_1}} (hc' : c' < aleph0) :
    toPartENat c ≤ toPartENat c' ↔ c ≤ c'
    source
    theorem Cardinal.toPartENat_inj_of_le_aleph0 {c c' : Cardinal.{u_1}} (hc : c ≤ aleph0) (hc' : c' ≤ aleph0) :
    toPartENat c = toPartENat c' ↔ c = c'
    source
    @[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.

    source
    theorem Cardinal.toPartENat_mono {c c' : Cardinal.{u_1}} (h : c ≤ c') :
    toPartENat c ≤ toPartENat c'
    source
    theorem Cardinal.toPartENat_lift (c : Cardinal.{v}) :
    toPartENat (lift.{u, v} c) = toPartENat c
    source
    theorem Cardinal.toPartENat_congr {α : Type u} {β : Type v} (e : α ≃ β) :
    toPartENat (mk α) = toPartENat (mk β)
    source
    theorem Cardinal.mk_toPartENat_eq_coe_card {α : Type u} [Fintype α] :
    toPartENat (mk α) = ↑(Fintype.card α)