Theorems · Theorem · general topology

Filter.Eventually.exists_Ioo_subset

∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α]
  {a : α} {p : α → Prop}, (∀ᶠ (x : α) in nhds a, p x) → ∃ l u, a ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ {x | p x}

Defined in

Mathlib.Topology.Order.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderTopologyNoMaxOrderNoMinOrder