Def RelIso.sumLexEmpty

Modification history

2025-07-05 10:59
Mathlib/Order/RelIso/Basic.lean
feat(Order/InitialSeg): `InitialSeg.exists_sum_relIso` (#26772) …
Added RelIso.sumLexEmptyView on Github →