Def RelIso.emptySumLex

Modification history

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