Theorems · Theorem · functional analysis
eq_of_norm_eq_of_norm_add_eq
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x y : E},
‖x‖ = ‖y‖ → ‖x + y‖ = ‖x‖ + ‖y‖ → x = yIf x and y are two vectors in a strictly convex space have the same norm and the norm of
their sum is equal to the sum of their norms, then they are equal.
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 167 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Realstatement and proof · cited by 25,697
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- Norm.normstatement and proof · cited by 5,413
- StrictConvexSpacestatement and proof · cited by 57
- sameRay_iff_norm_addproof · cited by 3
- SameRay.eq_of_norm_eqproof · cited by 2
Cited by5
Results whose statement or proof uses this declaration.
- Complex.affine_of_mapsTo_ball_of_norm_dslope_eq_divproof · cited by 2
- Complex.eqOn_of_isPreconnected_of_isMaxOn_normproof · cited by 2
- EuclideanGeometry.Sphere.isDiameter_iff_mem_and_mem_and_distproof · cited by 1
- Complex.eq_of_isMaxOn_of_ball_subsetproof · cited by 1
- MDifferentiableOn.eqOn_of_isPreconnected_of_isMaxOn_normproof · cited by 0