Theorem Ordinal.mk_le_of_forall_mk_setOfPred_lt

Modification history

2026-09-30 01:41
Mathlib/SetTheory/Ordinal/Basic.lean
chore: extract lemma from `Cardinal.mul_self` (#44006) …
Added Ordinal.mk_le_of_forall_mk_setOfPred_ltView on Github →