Commit 2024-11-04 13:07 500668ec

View on Github →

feat(Data/Real/Cardinality): Uncountable ℝ (#18546) We were somehow missing this spelling of that theorem.

Estimated changes

Modified Mathlib/Data/Real/Cardinality.lean

modified theorem Cardinal.not_countable_real

Modified Mathlib/Data/Set/Countable.lean

added theorem Set.not_countable_univ

added theorem Set.not_countable_univ_iff

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.aleph0_lt_mk

added theorem Cardinal.aleph0_lt_mk_iff