Theorems · Theorem · real analysis

Filter.Eventually.exists_lt

∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] {a : α} [(nhdsWithin a (Set.Iio a)).NeBot]
  {p : α → Prop}, (∀ᶠ (x : α) in nhds a, p x) → ∃ b < a, p b

Defined in

Mathlib.Topology.Order.LeftRight

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePreorderFilter.NeBot