Theorems · Theorem · functional analysis
norm_add_le
- #91 of the 100 theorems: The Triangle Inequality
∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), ‖a + b‖ ≤ ‖a‖ + ‖b‖Triangle inequality for the norm.
- Defined in
- Mathlib.Analysis.Normed.Group.Basic
- Cited by
- 68 results in Mathlib
- Foundations
- Depth 97 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.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Norm.normstatement and proof · cited by 5,413
- add_zeroproof · cited by 2,707
- zero_addproof · cited by 2,366
- neg_negproof · cited by 960
- neg_zeroproof · cited by 542
- SeminormedAddGroupstatement and proof · cited by 331
- dist_eq_norm_neg_addproof · cited by 46
- dist_triangleproof · cited by 44
Cited by69
Results whose statement or proof uses this declaration.
- norm_sub_leproof · cited by 26
- norm_sum_leproof · cited by 25
- norm_add_le_of_leproof · cited by 13
- norm_add₃_leproof · cited by 9
- MeasureTheory.DominatedFinMeasAdditive.add_measureproof · cited by 4
- norm_le_norm_add_norm_sub'proof · cited by 4
- IsMaxFilter.norm_add_sameRayproof · cited by 4
- norm_sub_le_norm_sub_add_norm_subproof · cited by 4
- MeasureTheory.DominatedFinMeasAdditive.addproof · cited by 3
- norm_le_norm_add_norm_neg_addproof · cited by 3
- norm_multiset_sum_leproof · cited by 3
- nnnorm_add_leproof · cited by 3