Theorems · Theorem · Lie groups
ENNReal.tendsto_coe
∀ {α : Type u} {f : Filter α} {m : α → NNReal} {a : NNReal},
Filter.Tendsto (fun a => ↑(m a)) f (nhds ↑a) ↔ Filter.Tendsto m f (nhds a)- Defined in
- Mathlib.Topology.Algebra.Ring.Real
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 129 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement · cited by 9,879
- Filterstatement and proof · cited by 8,121
- nhdsstatement · cited by 5,554
- NNRealstatement and proof · cited by 4,310
- Filter.Tendstostatement · cited by 3,814
- ENNReal.ofNNRealstatement · cited by 1,279
- Topology.IsEmbedding.tendsto_nhds_iffproof · cited by 13
- ENNReal.isEmbedding_coeproof · cited by 4
Cited by11
Results whose statement or proof uses this declaration.
- MeasureTheory.exists_eLpNorm_indicator_leproof · cited by 3
- MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_eLpNormproof · cited by 3
- MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀proof · cited by 2
- ENNReal.tendsto_tsum_compl_atTop_zeroproof · cited by 2
- Asymptotics.Filter.Tendsto.isBigOTVS_oneproof · cited by 1
- MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux2proof · cited by 1
- VitaliFamily.measure_limRatioMeas_zeroproof · cited by 1
- ENNReal.tendsto_cofinite_zero_of_tsum_ne_topproof · cited by 1
- VitaliFamily.withDensity_limRatioMeas_eqproof · cited by 1
- MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv_aux2proof · cited by 1
- MeasureTheory.addHaar_image_eq_zero_of_det_fderivWithin_eq_zeroproof · cited by 0