LeanPool.RlTheoryInLean.Analysis.Normed.Group.Basic

theorem norm_add_sq_le_norm_sq_add_norm_sq {E : Type u_1} [SeminormedAddGroup E] (x y : E) : ‖x + y‖ ^ 2 ≤ 2 * ‖x‖ ^ 2 + 2 * ‖y‖ ^ 2