Mathlib Map

Theorems · Theorem · real analysis

NNReal.coe_injective

Function.Injective NNReal.toReal
Defined in
Mathlib.Data.NNReal.Defs
Cited by
16 results in Mathlib
Foundations
Depth 97 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.

NNReal.coe_inj · cited by 30NNReal.coe_injMeasureTheory.Measure.addModularCharacterFun_eq_addHaarScalarFactor · cited by 3Measure.addModularCharact…MeasureTheory.Measure.modularCharacterFun_eq_haarScalarFactor · cited by 3Measure.modularCharacterF…MeasureTheory.Measure.addHaarScalarFactor_domSMul · cited by 3Measure.addHaarScalarFact…MeasureTheory.Measure.addHaarScalarFactor_self · cited by 3Measure.addHaarScalarFact…MeasureTheory.Measure.haarScalarFactor_self · cited by 3Measure.haarScalarFactor_…IsUltrametricDist.nnnorm_add_eq_max_of_nnnorm_ne_nnnorm · cited by 2IsUltrametricDist.nnnorm_…IsUltrametricDist.nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm · cited by 2IsUltrametricDist.nnnorm_…MeasureTheory.Measure.haarScalarFactor_smul · cited by 1Measure.haarScalarFactor_…Real.toNNReal_abs · cited by 1Real.toNNReal_absisProperMap_nndist · cited by 1isProperMap_nndistMeasureTheory.Measure.mul_addHaarScalarFactor_smul · cited by 1Measure.mul_addHaarScalar…MeasureTheory.Measure.mul_haarScalarFactor_smul · cited by 1Measure.mul_haarScalarFac…MeasureTheory.Measure.addHaarScalarFactor_smul · cited by 1Measure.addHaarScalarFact…IsUltrametricDist.nnnorm_div_eq_max_of_nnnorm_div_ne_nnnorm_div · cited by 0IsUltrametricDist.nnnorm_…Real · cited by 25697RealNNReal · cited by 4310NNRealNNReal.toReal · cited by 1260NNReal.toRealSubtype.coe_injective · cited by 205Subtype.coe_injectiveNNReal.coe_injectiveCITED BYCITES

Cites4

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.