Theorems · Theorem · general topology

mem_nhdsLE_iff_exists_Icc_subset

∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMinOrder α]
  [DenselyOrdered α] {a : α} {s : Set α}, s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l < a, Set.Icc l a ⊆ s

A set is a neighborhood of a within (-∞, a] if and only if it contains an interval [l, a] with l < a.

Defined in

Mathlib.Topology.Order.LeftRightNhds

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderTopologyNoMinOrderDenselyOrdered