Commit 2025-07-19 23:40 05f5869a

View on Github →

refactor(SetTheory/Ordinal/Arithmetic): redefine subtraction (#26889) We redefine ordinal subtraction so as to make add_sub_cancel_of_le an immediate corollary. This allows us to give a much simpler proof for add_le_iff_of_isSuccLimit.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

modified theorem Ordinal.add_le_iff_of_isSuccLimit

deleted theorem Ordinal.add_le_of_forall_add_lt

modified theorem Ordinal.add_sub_cancel

modified theorem Ordinal.le_add_sub

added theorem Ordinal.lt_add_iff_of_isSuccLimit

modified theorem Ordinal.sub_le

Modified Mathlib/SetTheory/Ordinal/Family.lean

deleted theorem Ordinal.lt_add_of_limit