Theorems · Theorem · general topology
Filter.eventuallyEq_iff_exists_mem
∀ {α : Type u} {β : Type v} {l : Filter α} {f g : α → β}, f =ᶠ[l] g ↔ ∃ s ∈ l, Set.EqOn f g s- Defined in
- Mathlib.Order.Filter.Basic
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Filterstatement and proof · cited by 8,121
- Filter.EventuallyEqstatement · cited by 1,912
- Set.EqOnstatement · cited by 603
- Filter.eventually_iff_exists_memproof · cited by 28
Cited by19
Results whose statement or proof uses this declaration.
- notMem_tsupport_iff_eventuallyEqproof · cited by 7
- CircleIntegrable.congr_codiscreteWithinproof · cited by 3
- LSeries_eventually_eq_zero_iff'proof · cited by 2
- LSeriesSummable.congr'proof · cited by 2
- ContinuousOn.continuousAt_indicatorproof · cited by 1
- DirichletCharacter.deriv_LFunctionTrivChar₁_apply_of_ne_oneproof · cited by 1
- AnalyticOnNhd.congrproof · cited by 1
- isMIntegralCurveOn_piecewiseproof · cited by 1
- isMIntegralCurve_abs_add_one_of_isMIntegralCurveOn_Iooproof · cited by 1
- UniformContinuousOn.comp_tendstoUniformly_eventuallyproof · cited by 1
- ODE_solution_unique_of_eventuallyproof · cited by 1
- CPolynomialOn.congrproof · cited by 1