Theorem Ordinal.IsNormal.le_apply

Modification history

2024-09-17 07:27
Mathlib/SetTheory/Ordinal/Arithmetic.lean
feat(Order/WellFounded): Generalize `StrictMono.id_le` (#16706) …
Added Ordinal.IsNormal.le_applyView on Github →