Documentation

Mathlib.Deprecated.Cardinal.Continuum

Deprecated material from Mathlib.SetTheory.Cardinal.Aleph and Mathlib.SetTheory.Cardinal.Continuum #

Moved here so we can reduce imports sooner.

source
@[simp, deprecated Cardinal.aleph_toENat]
theorem Cardinal.aleph_toPartENat (o : Ordinal.{u_1}) :
Cardinal.toPartENat (Cardinal.aleph o) = ⊤
source
@[simp, deprecated Cardinal.aleph_toENat]
theorem Cardinal.continuum_toPartENat :
Cardinal.toPartENat Cardinal.continuum = ⊤