Commit 2024-10-16 00:08 2ae1eb8b

View on Github →

feat(SetTheory/Cardinal/Aleph): add notation for aleph and beth (#17671)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

modified theorem Cardinal.aleph0_le_beth

modified theorem Cardinal.aleph0_lt_aleph_one

modified theorem Cardinal.aleph_eq_aleph'

modified theorem Cardinal.aleph_le

modified theorem Cardinal.aleph_le_beth

modified theorem Cardinal.aleph_limit

modified theorem Cardinal.aleph_lt

modified theorem Cardinal.aleph_max

modified theorem Cardinal.aleph_succ

modified theorem Cardinal.aleph_toNat

modified theorem Cardinal.aleph_toPartENat

modified theorem Cardinal.aleph_zero

modified theorem Cardinal.beth_le

modified theorem Cardinal.beth_limit

modified theorem Cardinal.beth_lt

modified theorem Cardinal.beth_ne_zero

modified theorem Cardinal.beth_pos

modified theorem Cardinal.beth_succ

modified theorem Cardinal.beth_zero

modified theorem Cardinal.countable_iff_lt_aleph_one

modified theorem Cardinal.max_aleph_eq

modified theorem Cardinal.ord_aleph_isLimit

modified theorem Cardinal.succ_aleph0

Modified Mathlib/SetTheory/Cardinal/Continuum.lean

modified theorem Cardinal.aleph_one_le_continuum

modified theorem Cardinal.beth_one

modified theorem Cardinal.two_power_aleph0