Theorem Cardinal.nat_lt_univ

Modification history

2026-04-07 10:49
Mathlib/SetTheory/Ordinal/Basic.lean
chore: move `Ordinal.univ` and `Cardinal.univ` to their own file (#37681) …
Modified Cardinal.nat_lt_univView on Github →
2026-01-21 17:08
Mathlib/SetTheory/Ordinal/Basic.lean
chore(SetTheory/Cardinal): remove explicit argument to `nat_lt_aleph0` (#33990) …
Modified Cardinal.nat_lt_univView on Github →
2025-07-06 21:54
Mathlib/SetTheory/Ordinal/Basic.lean
feat: simple lemmas on `Cardinal.univ` (#26818)
Added Cardinal.nat_lt_univView on Github →