Theorems · Theorem · general topology
Filter.EventuallyEq.le
∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {f g : α → β}, f =ᶠ[l] g → f ≤ᶠ[l] g- Defined in
- Mathlib.Order.Filter.Basic
- Cited by
- 46 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- Preorderstatement and proof · cited by 7,952
- Filter.EventuallyEqstatement and proof · cited by 1,912
- Filter.Eventually.monoproof · cited by 646
- Filter.EventuallyLEstatement · cited by 383
- le_of_eqproof · cited by 366
Cited by46
Results whose statement or proof uses this declaration.
- MeasureTheory.lintegral_congr_aeproof · cited by 95
- MeasureTheory.measure_congrproof · cited by 58
- MeasureTheory.Measure.restrict_congr_setproof · cited by 43
- MeasureTheory.Martingale.submartingaleproof · cited by 10
- Filter.EventuallyLE.reflproof · cited by 9
- MeasureTheory.Measure.ae_eq_set_piproof · cited by 9
- Filter.EventuallyLE.trans_eqproof · cited by 8
- MeasureTheory.Submartingale.negproof · cited by 7
- MeasureTheory.Measure.QuasiMeasurePreserving.preimage_ae_eqproof · cited by 5
- MeasureTheory.IntegrableOn.congr_set_aeproof · cited by 5
- Filter.EventuallyEq.countable_iUnionproof · cited by 4
- Filter.EventuallyEq.trans_leproof · cited by 4