Theorems · Theorem · general topology

Filter.EventuallyEq.of_forall_eventually_gt_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, x < f a ↔ x < g a) → f =ᶠ[l] g

Defined in

Mathlib.Topology.Order.CountableSeparating

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderTopologySecondCountableTopologyCountableInterFilter