Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-01-18 13:29
05dc8889
View on Github →
feat(Cardinal): define conversion to/from
ENat
(
#9792
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/SetTheory/Cardinal/ENat.lean
added
theorem
Cardinal.aleph0_add_ofENat
added
theorem
Cardinal.aleph0_mul_ofENat
added
theorem
Cardinal.enat_gc
added
theorem
Cardinal.lift_eq_ofENat
added
theorem
Cardinal.lift_le_ofENat
added
theorem
Cardinal.lift_lt_ofENat
added
theorem
Cardinal.lift_ofENat
added
theorem
Cardinal.nat_eq_ofENat
added
theorem
Cardinal.nat_le_ofENat
added
theorem
Cardinal.nat_lt_ofENat
added
def
Cardinal.ofENat
added
def
Cardinal.ofENatHom
added
theorem
Cardinal.ofENat_add
added
theorem
Cardinal.ofENat_add_aleph0
added
theorem
Cardinal.ofENat_eq_lift
added
theorem
Cardinal.ofENat_eq_nat
added
theorem
Cardinal.ofENat_eq_ofNat
added
theorem
Cardinal.ofENat_eq_one
added
theorem
Cardinal.ofENat_eq_zero
added
theorem
Cardinal.ofENat_inj
added
theorem
Cardinal.ofENat_injective
added
theorem
Cardinal.ofENat_le_aleph0
added
theorem
Cardinal.ofENat_le_lift
added
theorem
Cardinal.ofENat_le_nat
added
theorem
Cardinal.ofENat_le_ofENat
added
theorem
Cardinal.ofENat_le_ofNat
added
theorem
Cardinal.ofENat_le_one
added
theorem
Cardinal.ofENat_lt_aleph0
added
theorem
Cardinal.ofENat_lt_lift
added
theorem
Cardinal.ofENat_lt_nat
added
theorem
Cardinal.ofENat_lt_ofENat
added
theorem
Cardinal.ofENat_lt_ofNat
added
theorem
Cardinal.ofENat_mono
added
theorem
Cardinal.ofENat_mul
added
theorem
Cardinal.ofENat_mul_aleph0
added
theorem
Cardinal.ofENat_nat
added
theorem
Cardinal.ofENat_ofNat
added
theorem
Cardinal.ofENat_one
added
theorem
Cardinal.ofENat_pos
added
theorem
Cardinal.ofENat_strictMono
added
theorem
Cardinal.ofENat_toENat_eq_self
added
theorem
Cardinal.ofENat_toENat_le
added
theorem
Cardinal.ofENat_top
added
theorem
Cardinal.ofENat_zero
added
theorem
Cardinal.ofNat_eq_ofENat
added
theorem
Cardinal.ofNat_le_ofENat
added
theorem
Cardinal.ofNat_lt_ofENat
added
theorem
Cardinal.one_eq_ofENat
added
theorem
Cardinal.one_le_ofENat
added
theorem
Cardinal.one_lt_ofENat
added
theorem
Cardinal.range_ofENat
added
theorem
Cardinal.toENatAux_eq_nat
added
theorem
Cardinal.toENatAux_eq_top
added
theorem
Cardinal.toENatAux_eq_zero
added
theorem
Cardinal.toENatAux_gc
added
theorem
Cardinal.toENatAux_nat
added
theorem
Cardinal.toENatAux_ofENat
added
theorem
Cardinal.toENatAux_zero
added
theorem
Cardinal.toENat_comp_ofENat
added
theorem
Cardinal.toENat_eq_nat
added
theorem
Cardinal.toENat_eq_ofNat
added
theorem
Cardinal.toENat_eq_one
added
theorem
Cardinal.toENat_eq_top
added
theorem
Cardinal.toENat_eq_zero
added
theorem
Cardinal.toENat_injOn
added
theorem
Cardinal.toENat_nat
added
theorem
Cardinal.toENat_ofENat
added
theorem
Cardinal.toENat_strictMonoOn
added
theorem
Cardinal.toNat_toENat
added
theorem
Cardinal.zero_eq_ofENat