Theorems · Theorem · general topology
Filter.Tendsto.mono_left
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x y : Filter α} {z : Filter β},
Filter.Tendsto f x z → y ≤ x → Filter.Tendsto f y z- Defined in
- Mathlib.Order.Filter.Tendsto
- Cited by
- 125 results in Mathlib
- Foundations
- Depth 63 from the axioms, rests on 661 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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.Tendstostatement and proof · cited by 3,814
- LE.le.transproof · cited by 3,151
- Filter.map_monoproof · cited by 63
Cited by125
Results whose statement or proof uses this declaration.
- ContinuousOn.monoproof · cited by 156
- ContinuousWithinAt.monoproof · cited by 44
- tendsto_nhdsWithin_of_tendsto_nhdsproof · cited by 20
- exists_fun_of_mem_tangentConeAtproof · cited by 9
- ContinuousWithinAt.mono_of_mem_nhdsWithinproof · cited by 7
- not_continuousAt_of_tendstoproof · cited by 6
- tendsto_nhdsWithin_mono_leftproof · cited by 5
- interior_subset_gauge_lt_oneproof · cited by 5
- Filter.tendsto_iInf'proof · cited by 5
- hasSum_sum_of_ne_finset_zeroproof · cited by 5
- MeasureTheory.addHaar_image_le_mul_of_det_ltproof · cited by 4
- MeasureTheory.exists_Lp_halfproof · cited by 4