Theorem InfClosed.insert_lowerBounds

Modification history

2026-06-03 10:30
Mathlib/Order/SupClosed.lean
chore: use `to_dual` for `SupClosed`/`InfClosed` (#40175) …
Deleted InfClosed.insert_lowerBoundsView on Github →
2024-11-23 09:23
Mathlib/Order/SupClosed.lean
feature(Order/SupClosed): Add lemmas for inserting upper or lower bounds into a Sup/Inf closed set (#18740) …
Added InfClosed.insert_lowerBoundsView on Github →