Theorem InitialSeg.exists_sum_relIso

Modification history

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