Theorems · Theorem · general topology
ENNReal.Tendsto.const_mul
∀ {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a b : ENNReal},
Filter.Tendsto m f (nhds b) → b ≠ 0 ∨ a ≠ ⊤ → Filter.Tendsto (fun b => a * m b) f (nhds (a * b))- Cited by
- 13 results in Mathlib
- Foundations
- Depth 137 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement and proof · cited by 9,879
- Top.topstatement and proof · cited by 9,680
- Filterstatement and proof · cited by 8,121
- nhdsstatement and proof · cited by 5,554
- Filter.Tendstostatement and proof · cited by 3,814
- MulZeroClass.zero_mulproof · cited by 1,625
- tendsto_const_nhdsproof · cited by 330
- by_casesproof · cited by 31
- ENNReal.Tendsto.mulproof · cited by 9
Cited by13
Results whose statement or proof uses this declaration.
- ENNReal.tsum_mul_leftproof · cited by 21
- ENNReal.Tendsto.mul_constproof · cited by 14
- MeasureTheory.addHaar_image_le_mul_of_det_ltproof · cited by 4
- MeasureTheory.exists_Lp_halfproof · cited by 4
- ENNReal.eq_zero_of_le_mul_powproof · cited by 2
- MeasureTheory.OuterMeasure.mkMetric_mono_smulproof · cited by 2
- ENNReal.tendsto_const_mul_rpow_nhds_zero_of_posproof · cited by 2
- MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurableproof · cited by 1
- MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux2proof · cited by 1
- ENNReal.continuousAt_const_mulproof · cited by 1
- MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv_aux2proof · cited by 1
- MeasureTheory.VectorMeasure.Integrable.tendsto_setIntegral_nhds_zeroproof · cited by 0