Theorem Ico_mem_nhdsGE

Modification history

2026-04-07 22:06

Mathlib/Topology/Order/OrderClosed.lean

chore(Topology/Order/OrderClosed): use `to_dual` (#35638)

Deleted Ico_mem_nhdsGE View on Github →

2024-12-23 08:37

Mathlib/Topology/Order/OrderClosed.lean

chore(*): rename lemmas about `𝓝[≥] a` etc (#20188) …

Added Ico_mem_nhdsGE View on Github →