Mathlib Map

Theorems · Theorem · real analysis

NNReal.zero_le_coe

∀ {q : NNReal}, 0 ≤ ↑q
Defined in
Mathlib.Data.NNReal.Defs
Cited by
13 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.

RealRMK.rieszMeasure_le_of_eq_one · cited by 3RealRMK.rieszMeasure_le_o…Metric.isCover_iff_subset_cthickening · cited by 3Metric.isCover_iff_subset…NNReal.spectralRadius_mem_spectrum · cited by 2NNReal.spectralRadius_mem…Real.toNNReal_add_le · cited by 2Real.toNNReal_add_leNNReal.continuous_nnrpow_const · cited by 1NNReal.continuous_nnrpow_…eHolderNorm_eq_zero · cited by 1eHolderNorm_eq_zeroMeasureTheory.Measure.HasTemperateGrowth.exists_eLpNorm_lt_top · cited by 1HasTemperateGrowth.exists…NNReal.monotone_nnrpow_const · cited by 1NNReal.monotone_nnrpow_co…NNReal.indicator_summable · cited by 1NNReal.indicator_summableStieltjesFunction.measure_smul · cited by 0StieltjesFunction.measure…Metric.IsCover.of_subset_cthickening_of_lt · cited by 0IsCover.of_subset_cthicke…SchwartzMap.norm_toLp_le_seminorm · cited by 0SchwartzMap.norm_toLp_le_…CFC.rpow_sqrt_nnreal · cited by 0CFC.rpow_sqrt_nnrealReal · cited by 25697RealNNReal · cited by 4310NNRealNNReal.toReal · cited by 1260NNReal.toRealNNReal.zero_le_coeCITED BYCITES

Cites3

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

  • Realstatement · cited by 25,697
  • NNRealstatement and proof · cited by 4,310
  • NNReal.toRealstatement · cited by 1,260

Cited by13

Results whose statement or proof uses this declaration.