Commit 2022-01-25 22:24 b237af52

View on Github →

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.

Estimated changes

Modified src/set_theory/ordinal_arithmetic.lean

added theorem ordinal.blsub_le

deleted theorem ordinal.blsub_le_iff_lt

added theorem ordinal.lsub_le

deleted theorem ordinal.lsub_le_iff_lt