Theorem Ordinal.mem_range_lift_of_le

Modification history

2024-10-22 17:45
Mathlib/SetTheory/Ordinal/Basic.lean
chore(SetTheory/Ordinal/Basic): golf `Ordinal.lift` lemmas (#17517) …
Added Ordinal.mem_range_lift_of_leView on Github →