Theorems · Theorem · general topology

Filter.EventuallyEq.of_forall_eventually_le_iff

∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LinearOrder X] [OrderTopology X] [SecondCountableTopology X]
  {α : Type u_2} {l : Filter α} [CountableInterFilter l] {f g : α → X},
  (∀ (x : X), ∀ᶠ (a : α) in l, f a ≤ x ↔ g a ≤ x) → f =ᶠ[l] g

Defined in

Mathlib.Topology.Order.CountableSeparating

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderTopologySecondCountableTopologyCountableInterFilter