Theorems · Theorem · general topology

eventually_const_le_iff_forall_lt_eventually_const_lt

∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [FirstCountableTopology α] {l : Filter γ} [CountableInterFilter l] {f : γ → α} {a : α},
  (∀ᶠ (x : γ) in l, a ≤ f x) ↔ ∀ b < a, ∀ᶠ (x : γ) in l, b < f x

Defined in

Mathlib.Topology.Order.IsLUB

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderTopologyFirstCountableTopologyCountableInterFilter