Theorem Cardinal.ord_eq_iInf

Modification history

2026-03-20 04:53
Mathlib/SetTheory/Ordinal/Basic.lean
chore: `no_expose` various `Ordinal` definitions (#34729) …
Added Cardinal.ord_eq_iInfView on Github →