Theorem PrincipalSeg.down

Modification history

2025-04-11 00:24
Mathlib/Order/InitialSeg.lean
chore: delete >6 month old deprecations (2024-10 01-10) (#23928) …
Deleted PrincipalSeg.downView on Github →
2022-12-14 23:20
Mathlib/Order/InitialSeg.lean
feat port: Order.InitialSeg (#1012) …
Added PrincipalSeg.downView on Github →