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.
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 : Cardinal.{u_1}} {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 : Cardinal.{u_1}} {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 : Cardinal.{u_1}} {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 : Cardinal.{u_1}} {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 α)