Commit 2024-11-19 02:51 47f0d27a

View on Github →

chore(SetTheory/Cardinal/Aleph): golf aleph theorems (#18204)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

added theorem Cardinal.preAleph_le_aleph

modified theorem Cardinal.preAleph_nat

modified theorem Cardinal.preAleph_omega0

added theorem Ordinal.preOmega_le_omega