Theorem wellFounded_iff_principalSeg.{u}

Modification history

2025-07-05 10:59
Mathlib/Order/InitialSeg.lean
feat(Order/InitialSeg): `InitialSeg.exists_sum_relIso` (#26772) …
Deleted wellFounded_iff_principalSeg.{u}View on Github →
2023-03-31 17:01
Mathlib/Order/InitialSeg.lean
feat: port #18527 (#3190) …
Added wellFounded_iff_principalSeg.{u}View on Github →