mathlib3
b237af52 - refactor(set_theory/ordinal_arithmetic): Rename `lsub_le_iff_lt` to `lsub_le` (#11661)

Commit

3 years ago

refactor(set_theory/ordinal_arithmetic): Rename `lsub_le_iff_lt` to `lsub_le` (#11661) This way, it directly corresponds to `sup_le`. Ditto for `blsub_le_iff_lt`.

Author

vihdzp

Parents

b0a18124

mathlib3 b237af52 - refactor(set_theory/ordinal_arithmetic): Rename `lsub_le_iff_lt` to `lsub_le` (#11661)

mathlib3
b237af52 - refactor(set_theory/ordinal_arithmetic): Rename `lsub_le_iff_lt` to `lsub_le` (#11661)