Theorem SupClosed.insert_upperBounds

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_upperBoundsView on Github →