Theorems · Theorem · general topology
ENNReal.Tendsto.mul_const
∀ {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a b : ENNReal},
Filter.Tendsto m f (nhds a) → a ≠ 0 ∨ b ≠ ⊤ → Filter.Tendsto (fun x => m x * b) f (nhds (a * b))- Cited by
- 14 results in Mathlib
- Foundations
- Depth 138 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- mul_commproof · cited by 2,262
- ENNReal.Tendsto.const_mulproof · cited by 13
Cited by14
Results whose statement or proof uses this declaration.
- ENNReal.tsum_const_eq_top_of_ne_zeroproof · cited by 4
- BoundedVariationOn.tendsto_eVariationOn_Ici_zero_of_filterproof · cited by 3
- MeasureTheory.measure_univ_of_isAddLeftInvariantproof · cited by 2
- VitaliFamily.measure_limRatioMeas_topproof · cited by 2
- ENNReal.Tendsto.div_constproof · cited by 2
- ENNReal.continuousAt_mul_constproof · cited by 2
- Besicovitch.exists_disjoint_closedBall_covering_ae_of_finiteMeasure_auxproof · cited by 1
- MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux2proof · cited by 1
- MeasureTheory.measure_univ_of_isMulLeftInvariantproof · cited by 1
- VitaliFamily.measure_limRatioMeas_zeroproof · cited by 1
- bergelson'proof · cited by 1
- VitaliFamily.withDensity_limRatioMeas_eqproof · cited by 1