Theorems · Theorem · general topology
Filter.eventuallyLE_antisymm_iff
∀ {α : Type u} {β : Type v} [inst : PartialOrder β] {l : Filter α} {f g : α → β}, f =ᶠ[l] g ↔ f ≤ᶠ[l] g ∧ g ≤ᶠ[l] f- Defined in
- Mathlib.Order.Filter.Basic
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses propext, Quot.sound
- Assumes
- PartialOrder
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.
- Filterstatement and proof · cited by 8,121
- PartialOrderstatement and proof · cited by 6,410
- Filter.Eventuallyproof · cited by 3,134
- Filter.EventuallyEqstatement · cited by 1,912
- Filter.EventuallyLEstatement · cited by 383
Cited by8
Results whose statement or proof uses this declaration.
- MeasureTheory.ae_eq_of_ae_subset_of_measure_geproof · cited by 3
- MeasureTheory.union_ae_eq_left_iff_ae_subsetproof · cited by 2
- blimsup_cthickening_mul_ae_eqproof · cited by 2
- MeasureTheory.vadd_set_ae_eqproof · cited by 1
- ProbabilityTheory.Kernel.ae_null_of_compProd_nullproof · cited by 1
- ProbabilityTheory.Kernel.ae_null_of_comp_nullproof · cited by 1
- MeasureTheory.Measure.measure_ae_null_of_prod_nullproof · cited by 1
- blimsup_cthickening_ae_eq_blimsup_thickeningproof · cited by 1