Theorem IsGLB.range_of_tendsto

Modification history

2026-04-07 22:06
Mathlib/Topology/Order/OrderClosed.lean
chore(Topology/Order/OrderClosed): use `to_dual` (#35638)
Deleted IsGLB.range_of_tendstoView on Github →
2024-11-22 00:49
Mathlib/Topology/Order/OrderClosed.lean
chore(Topology/Order): move&generalize 4 lemmas (#19238) …
Added IsGLB.range_of_tendstoView on Github →