Theorem SupClosed.insert_lowerBounds

Modification history

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 SupClosed.insert_lowerBoundsView on Github →