Theorems · Theorem · functional analysis
enorm_add_le
∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ESeminormedAddMonoid E] (a b : E), ‖a + b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ- Defined in
- Mathlib.Analysis.Normed.Group.Basic
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- ENNRealstatement · cited by 9,879
- ENorm.enormstatement · cited by 715
- ESeminormedAddMonoidstatement and proof · cited by 133
- ESeminormedAddMonoid.enorm_add_leproof · cited by 1
Cited by11
Results whose statement or proof uses this declaration.
- MeasureTheory.VectorMeasure.variation_add_leproof · cited by 4
- BoundedVariationOn.bilinear_compproof · cited by 3
- HasFPowerSeriesWithinOnBall.changeOriginproof · cited by 3
- HasFiniteFPowerSeriesOnBall.changeOriginproof · cited by 2
- enorm_add_le_of_leproof · cited by 2
- MeasureTheory.Integrable.add'proof · cited by 2
- enorm_sum_leproof · cited by 2
- enorm_add₃_leproof · cited by 1
- MeasureTheory.VectorMeasure.variation_withDensity'proof · cited by 1
- MeasureTheory.eLpNormEssSup_add_leproof · cited by 0
- enorm_multisetSum_leproof · cited by 0