Mathlib Map

Theorems · Theorem · functional analysis

Real.norm_of_nonneg

∀ {r : ℝ}, 0 ≤ r → ‖r‖ = r
Defined in
Mathlib.Analysis.Normed.Group.Real
Cited by
135 results in Mathlib
Foundations
Depth 106 from the axioms, rests on 2,310 definitions · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

norm_norm · cited by 113norm_normReal.enorm_eq_ofReal · cited by 16Real.enorm_eq_ofRealMeasureTheory.integrable_of_le_of_le · cited by 6MeasureTheory.integrable_…NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace · cited by 6mixedEmbedding.normAtPlac…MeasureTheory.Integrable.convolution_integrand · cited by 6Integrable.convolution_in…Real.nnnorm_of_nonneg · cited by 6Real.nnnorm_of_nonnegExistsContDiffBumpBase.w_support · cited by 4ExistsContDiffBumpBase.w_…AkraBazziRecurrence.eventually_bi_mul_le_r · cited by 4AkraBazziRecurrence.event…PhragmenLindelof.quadrant_I · cited by 4PhragmenLindelof.quadrant…MeasureTheory.Integrable.integral_comp · cited by 4Integrable.integral_compMeasureTheory.Integrable.integral_compProd · cited by 4Integrable.integral_compP…exists_norm_eq · cited by 4exists_norm_eqEisensteinSeries.summable_one_div_norm_rpow · cited by 4EisensteinSeries.summable…SchwartzMap.isBigO_cocompact_rpow · cited by 3SchwartzMap.isBigO_cocomp…ae_eq_zero_of_integral_contMDiff_smul_eq_zero · cited by 3ae_eq_zero_of_integral_co…Real · cited by 25697RealNorm.norm · cited by 5413Norm.normabs_of_nonneg · cited by 279abs_of_nonnegReal.norm_of_nonnegCITED BYCITES

Cites3

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

Cited by135

Results whose statement or proof uses this declaration.