HepLean Documentation

Mathlib.SetTheory.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}) :
    ↑(Cardinal.toENat c) = Cardinal.toPartENat c
    source
    @[simp]
    theorem Cardinal.toPartENat_natCast (n : ℕ) :
    Cardinal.toPartENat ↑n = ↑n
    source
    theorem Cardinal.toPartENat_apply_of_lt_aleph0 {c : Cardinal.{u_1}} (h : c < Cardinal.aleph0) :
    Cardinal.toPartENat c = ↑(Cardinal.toNat c)
    source
    theorem Cardinal.toPartENat_eq_top {c : Cardinal.{u_1}} :
    Cardinal.toPartENat c = ⊤ ↔ Cardinal.aleph0 ≤ c
    source
    theorem Cardinal.toPartENat_apply_of_aleph0_le {c : Cardinal.{u_1}} (h : Cardinal.aleph0 ≤ c) :
    Cardinal.toPartENat c = ⊤
    source
    @[deprecated Cardinal.toPartENat_natCast]
    theorem Cardinal.toPartENat_cast (n : ℕ) :
    Cardinal.toPartENat ↑n = ↑n

    Alias of Cardinal.toPartENat_natCast.

    source
    @[simp]
    theorem Cardinal.mk_toPartENat_of_infinite {α : Type u} [h : Infinite α] :
    Cardinal.toPartENat (Cardinal.mk α) = ⊤
    source
    @[simp]
    theorem Cardinal.aleph0_toPartENat :
    Cardinal.toPartENat Cardinal.aleph0 = ⊤
    source
    theorem Cardinal.toPartENat_surjective :
    Function.Surjective ⇑Cardinal.toPartENat
    source
    @[deprecated Cardinal.toPartENat_eq_top]
    theorem Cardinal.toPartENat_eq_top_iff_le_aleph0 {c : Cardinal.{u_1}} :
    Cardinal.toPartENat c = ⊤ ↔ Cardinal.aleph0 ≤ c

    Alias of Cardinal.toPartENat_eq_top.

    source
    theorem Cardinal.toPartENat_strictMonoOn :
    StrictMonoOn (⇑Cardinal.toPartENat) (Set.Iic Cardinal.aleph0)
    source
    theorem Cardinal.toPartENat_le_iff_of_le_aleph0 {c c' : Cardinal.{u_1}} (h : c ≤ Cardinal.aleph0) :
    Cardinal.toPartENat c ≤ Cardinal.toPartENat c' ↔ c ≤ c'
    source
    theorem Cardinal.toPartENat_le_iff_of_lt_aleph0 {c c' : Cardinal.{u_1}} (hc' : c' < Cardinal.aleph0) :
    Cardinal.toPartENat c ≤ Cardinal.toPartENat c' ↔ c ≤ c'
    source
    theorem Cardinal.toPartENat_eq_iff_of_le_aleph0 {c c' : Cardinal.{u_1}} (hc : c ≤ Cardinal.aleph0) (hc' : c' ≤ Cardinal.aleph0) :
    Cardinal.toPartENat c = Cardinal.toPartENat c' ↔ c = c'
    source
    theorem Cardinal.toPartENat_mono {c c' : Cardinal.{u_1}} (h : c ≤ c') :
    Cardinal.toPartENat c ≤ Cardinal.toPartENat c'
    source
    theorem Cardinal.toPartENat_lift (c : Cardinal.{v}) :
    Cardinal.toPartENat (Cardinal.lift.{u, v} c) = Cardinal.toPartENat c
    source
    theorem Cardinal.toPartENat_congr {α : Type u} {β : Type v} (e : α ≃ β) :
    Cardinal.toPartENat (Cardinal.mk α) = Cardinal.toPartENat (Cardinal.mk β)
    source
    theorem Cardinal.mk_toPartENat_eq_coe_card {α : Type u} [Fintype α] :
    Cardinal.toPartENat (Cardinal.mk α) = ↑(Fintype.card α)