Theorem Order.IsNormal.of_mem_lowerBounds_upperBounds

Modification history

2026-01-15 12:34
Mathlib/Order/IsNormal.lean
chore: remove declarations deprecated between 2021-01-15 and 2025-07-15 (#33988) …
Deleted Order.IsNormal.of_mem_lowerBounds_upperBoundsView on Github →
2025-04-03 11:14
Mathlib/Order/IsNormal.lean
feat: generalize normal functions (#20504) …
Added Order.IsNormal.of_mem_lowerBounds_upperBoundsView on Github →