Mathlib Map

Theorems · Theorem · general topology

continuous_real_toNNReal

Continuous Real.toNNReal
Defined in
Mathlib.Topology.Instances.NNReal.Lemmas
Cited by
15 results in Mathlib
Foundations
Depth 120 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ContinuousMap.realToNNReal · cited by 44ContinuousMap.realToNNRealENNReal.continuous_ofReal · cited by 16ENNReal.continuous_ofRealReal.continuous_sqrt · cited by 6Real.continuous_sqrtNNReal.coe_tsum · cited by 6NNReal.coe_tsumIsGreatest.nnnorm_cfcₙ_nnreal · cited by 5IsGreatest.nnnorm_cfcₙ_nn…IsGreatest.nnnorm_cfc_nnreal · cited by 5IsGreatest.nnnorm_cfc_nnr…ContinuousOn.ofReal_map_toNNReal · cited by 3ContinuousOn.ofReal_map_t…measurable_real_toNNReal · cited by 3measurable_real_toNNRealMeasureTheory.AEStronglyMeasurable.real_toNNReal · cited by 2AEStronglyMeasurable.real…cfc_tsub · cited by 1cfc_tsubNNReal.continuousAt_rpow · cited by 1NNReal.continuousAt_rpowCompletelyRegularSpace.exists_BCNN · cited by 1CompletelyRegularSpace.ex…tendsto_real_toNNReal · cited by 0tendsto_real_toNNRealMeasureTheory.StronglyMeasurable.real_toNNReal · cited by 0StronglyMeasurable.real_t…MeasureTheory.IsLocallyFiniteMeasure.withDensity_ofReal · cited by 0IsLocallyFiniteMeasure.wi…Real · cited by 25697RealNNReal · cited by 4310NNRealContinuous · cited by 2592Continuouscontinuous_const · cited by 278continuous_constReal.toNNReal · cited by 267Real.toNNRealcontinuous_id · cited by 192continuous_idContinuous.subtype_mk · cited by 51Continuous.subtype_mkContinuous.max · cited by 7Continuous.maxcontinuous_real_toNNRealCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by16

Results whose statement or proof uses this declaration.