Mathlib Map

Theorems · Theorem · real analysis

NNReal.coe_le_coe

∀ {r₁ r₂ : NNReal}, ↑r₁ ≤ ↑r₂ ↔ r₁ ≤ r₂
Defined in
Mathlib.Data.NNReal.Defs
Cited by
73 results in Mathlib
Foundations
Depth 105 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.

Summable.of_nonneg_of_le · cited by 36Summable.of_nonneg_of_leNNReal.coe_mono · cited by 13NNReal.coe_monoReal.sqrt_le_sqrt_iff · cited by 6Real.sqrt_le_sqrt_iffhasFDerivAt_integral_of_dominated_of_fderiv_le · cited by 5hasFDerivAt_integral_of_d…ContinuousMultilinearMap.le_opNNNorm · cited by 5ContinuousMultilinearMap.…Real.sqrt_le_sqrt · cited by 5Real.sqrt_le_sqrtReal.le_toNNReal_iff_coe_le · cited by 5Real.le_toNNReal_iff_coe_…hasDerivAt_integral_of_dominated_loc_of_deriv_le · cited by 4hasDerivAt_integral_of_do…nnnorm_sum_le · cited by 4nnnorm_sum_leNNReal.exists_pos_sum_of_countable · cited by 4NNReal.exists_pos_sum_of_…NNReal.hasSum_lt · cited by 3NNReal.hasSum_ltcontentRegular_rieszContent · cited by 3contentRegular_rieszConte…nnnorm_add_le · cited by 3nnnorm_add_leHolderOnWith.of_le · cited by 2HolderOnWith.of_leMeasureTheory.Measure.measure_preimage_isAddLeftInvariant_eq_smul_of_hasCompactSupport · cited by 2Measure.measure_preimage_…Real · cited by 25697RealNNReal · cited by 4310NNRealNNReal.toReal · cited by 1260NNReal.toRealNNReal.coe_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 by73

Results whose statement or proof uses this declaration.