Theorems · Theorem · general topology

TFAE_mem_nhdsGE

∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a b : α},
  a < b →
    ∀ (s : Set α),
      [s ∈ nhdsWithin a (Set.Ici a), s ∈ nhdsWithin a (Set.Icc a b), s ∈ nhdsWithin a (Set.Ico a b),
          ∃ u ∈ Set.Ioc a b, Set.Ico a u ⊆ s, ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s].TFAE

The following statements are equivalent: 0. s is a neighborhood of a within [a, +∞); 1. s is a neighborhood of a within [a, b]; 2. s is a neighborhood of a within [a, b); 3. s includes [a, u) for some u ∈ (a, b]; 4. s includes [a, u) for some u > a.

Defined in

Mathlib.Topology.Order.LeftRightNhds

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderTopology