Theorems · Theorem · general topology

mem_nhdsGT_iff_exists_Ioo_subset

∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMaxOrder α] {a : α}
  {s : Set α}, s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s

A set is a neighborhood of a within (a, +∞) if and only if it contains an interval (a, u) with a < u.

Defined in

Mathlib.Topology.Order.LeftRightNhds

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderTopologyNoMaxOrder