Theorems · Definition · general topology
Filter.EventuallyLE
{α : Type u_1} → {β : Type u_2} → [LE β] → Filter α → (α → β) → (α → β) → PropA function f is eventually less than or equal to a function g at a filter l.
- Defined in
- Mathlib.Order.Filter.Defs
- Cited by
- 383 results in Mathlib
- Foundations
- Depth 6 from the axioms, rests on 14 definitions · uses no axioms
- Assumes
- LE
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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.Eventuallyproof · cited by 3,134
Cited by389
Results whose statement or proof uses this declaration.
- MeasureTheory.Submartingaleproof · cited by 63
- Filter.EventuallyEq.lestatement · cited by 46
- MeasureTheory.integral_eq_lintegral_of_nonneg_aestatement and proof · cited by 31
- Filter.EventuallyLE.transstatement and proof · cited by 27
- Filter.EventuallyLE.antisymmstatement and proof · cited by 23
- MeasureTheory.Supermartingaleproof · cited by 23
- MeasureTheory.ofReal_integral_eq_lintegral_ofRealstatement and proof · cited by 22
- LE.le.eventuallyLEstatement · cited by 21
- MeasureTheory.integral_nonneg_of_aestatement and proof · cited by 17
- Filter.tendsto_atTop_mono'statement and proof · cited by 17
- MeasureTheory.integral_mono_of_nonnegstatement and proof · cited by 16
- Filter.limsup_le_limsupstatement and proof · cited by 16
Showing the 200 most cited of 389.