Theorems · Theorem · general topology

nhds_order_unbounded

∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] {a : α},
  (∃ u, a < u) → (∃ l, l < a) → nhds a = ⨅ l, ⨅ (_ : l < a), ⨅ u, ⨅ (_ : a < u), Filter.principal (Set.Ioo l u)

Defined in

Mathlib.Topology.Order.Basic

Cited by

1 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpacePreorderOrderTopology