Theorems · Theorem · general topology

Ioc_mem_nhdsLE_of_mem

∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b c : α},
  b ∈ Set.Ioc a c → Set.Ioc a c ∈ nhdsWithin b (Set.Iic b)

Defined in

Mathlib.Topology.Order.OrderClosed

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderClosedIicTopology