Theorem Cardinal.aleph0_lt_mk

Modification history

2024-11-04 13:07
Mathlib/SetTheory/Cardinal/Basic.lean
feat(Data/Real/Cardinality): `Uncountable ℝ` (#18546) …
Added Cardinal.aleph0_lt_mkView on Github →