Commit 2025-07-05 10:59 bfdf54ea

View on Github →

feat(Order/InitialSeg): InitialSeg.exists_sum_relIso (#26772) If r ≼i s, there exists some t with Sum.Lex r t ≃r s. In other words, ordinal subtraction exists.

Estimated changes

Modified Mathlib/Order/InitialSeg.lean

added theorem InitialSeg.exists_sum_relIso

deleted theorem wellFounded_iff_principalSeg.{u}

added theorem wellFounded_iff_principalSeg

Modified Mathlib/Order/RelIso/Basic.lean

added def RelIso.emptySumLex

added def RelIso.sumLexEmpty

Modified Mathlib/SetTheory/Ordinal/Basic.lean