Theorems · Theorem · general topology
Filter.EventuallyEq.symm
∀ {α : Type u} {β : Type v} {f g : α → β} {l : Filter α}, f =ᶠ[l] g → g =ᶠ[l] f- Defined in
- Mathlib.Order.Filter.Basic
- Cited by
- 408 results in Mathlib
- Foundations
- Depth 11 from the axioms, rests on 27 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Filterstatement and proof · cited by 8,121
- Filter.EventuallyEqstatement and proof · cited by 1,912
- Filter.Eventually.monoproof · cited by 646
Cited by408
Results whose statement or proof uses this declaration.
- MeasureTheory.lintegral_congr_aeproof · cited by 95
- MeasureTheory.integral_mapproof · cited by 67
- MeasureTheory.measure_congrproof · cited by 58
- MeasureTheory.Measure.restrict_congr_setproof · cited by 43
- MeasureTheory.integrable_congrproof · cited by 42
- MeasureTheory.integrable_condExpproof · cited by 28
- MeasureTheory.ofReal_integral_eq_lintegral_ofRealproof · cited by 22
- tendsto_nhds_of_eventually_eqproof · cited by 21
- MeasureTheory.Measure.map_smulproof · cited by 21
- meromorphicOrderAt_eq_top_iffproof · cited by 20
- MeasureTheory.AEStronglyMeasurable.congrproof · cited by 19
- MeasureTheory.condExp_congr_aeproof · cited by 17
Showing the 200 most cited of 408.