Theorems · Theorem · functional analysis
ofReal_norm
∀ {E : Type u_5} [inst : SeminormedAddGroup E] (x : E), ENNReal.ofReal ‖x‖ = ‖x‖ₑ- Defined in
- Mathlib.Analysis.Normed.Group.Basic
- Cited by
- 39 results in Mathlib
- Foundations
- Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SeminormedAddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement · cited by 9,879
- Norm.normstatement · cited by 5,413
- ENNReal.ofRealstatement · cited by 863
- norm_nonnegproof · cited by 725
- ENorm.enormstatement · cited by 715
- SeminormedAddGroupstatement and proof · cited by 331
- ENNReal.ofReal_eq_coe_nnrealproof · cited by 10
Cited by39
Results whose statement or proof uses this declaration.
- edist_eq_enorm_subproof · cited by 37
- Real.enorm_eq_ofRealproof · cited by 16
- MeasureTheory.tendsto_setToFun_of_dominated_convergenceproof · cited by 5
- enorm_le_iff_norm_leproof · cited by 4
- MeasureTheory.MemLp.eLpNorm_eq_integral_rpow_normproof · cited by 4
- MeasureTheory.VectorMeasure.norm_integral_le_lintegral_normproof · cited by 3
- MeasureTheory.integral_norm_eq_lintegral_enormproof · cited by 3
- MeasureTheory.L1.norm_eq_integral_normproof · cited by 3
- MeasureTheory.ae_tendsto_ofReal_normproof · cited by 2
- MeasureTheory.integrable_sum_measureproof · cited by 2
- MeasureTheory.eLpNorm_indicator_sub_le_of_dist_bddproof · cited by 2
- MeasureTheory.hasFiniteIntegral_iff_normproof · cited by 2