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.
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.