Theorems · Theorem · general topology
Filter.EventuallyEq.filter_mono
∀ {α : Type u} {β : Type v} {l l' : Filter α} {f g : α → β}, f =ᶠ[l] g → l' ≤ l → f =ᶠ[l'] g- Defined in
- Mathlib.Order.Filter.Basic
- Cited by
- 59 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext, Quot.sound
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
- Set.ofPredproof · cited by 6,101
- Filter.EventuallyEqstatement and proof · cited by 1,912
Cited by59
Results whose statement or proof uses this declaration.
- MeromorphicNFAt.meromorphicOrderAt_eq_zero_iffproof · cited by 14
- Set.EqOn.eventuallyEq_of_memproof · cited by 12
- HasDerivAt.congr_of_eventuallyEqproof · cited by 8
- ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNEproof · cited by 6
- fderivWithin_congrproof · cited by 4
- fderivWithin_congr_setproof · cited by 4
- toMeromorphicNFAt_eq_selfproof · cited by 4
- MeromorphicOn.intervalIntegrable_log_normproof · cited by 4
- hasFDerivWithinAt_congr_setproof · cited by 4
- MeasureTheory.Measure.AbsolutelyContinuous.prodproof · cited by 3
- Filter.EventuallyEq.restrictproof · cited by 3
- Filter.EventuallyEq.fderivWithin_eq_of_nhdsproof · cited by 3