Theorems · Theorem · general topology

eventually_le_const_iff_forall_gt_eventually_lt_const

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

Defined in

Mathlib.Topology.Order.IsLUB

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderTopologyFirstCountableTopologyCountableInterFilter