Theorem wellFounded_iff_principalSeg

Modification history

2025-07-05 10:59

Mathlib/Order/InitialSeg.lean

feat(Order/InitialSeg): `InitialSeg.exists_sum_relIso` (#26772) …

Added wellFounded_iff_principalSeg View on Github →