Theorems · Theorem · functional analysis
norm_add_sub_norm_sub_le_two_mul_min
∀ {E : Type u_8} [inst : SeminormedAddCommGroup E] (u v : E), ‖u + v‖ - ‖u - v‖ ≤ 2 * min ‖u‖ ‖v‖- Defined in
- Mathlib.Analysis.Normed.Group.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SeminormedAddCommGroup
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 and proof · cited by 25,697
- Norm.normstatement and proof · cited by 5,413
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- add_commproof · cited by 1,535
- le_of_ltproof · cited by 1,175
- norm_sub_revproof · cited by 41
- le_minproof · cited by 21
- mul_min_of_nonnegproof · cited by 2
- norm_add_sub_norm_sub_le_two_mulproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- ProbabilityTheory.measure_le_mul_measure_gt_le_of_map_rotation_eq_selfproof · cited by 1