parallelogram_law_with_nnnorm — Mathlib

English

In any inner product space, with NNReal norms, the parallelogram law holds: ‖x+y‖₊^2 + ‖x−y‖₊^2 = 2(‖x‖₊^2 + ‖y‖₊^2).

Русский

Величины для nnnorm удовлетворяют параллелограммовому тождеству: ‖x+y‖₊^2 + ‖x−y‖₊^2 = 2(‖x‖₊^2 + ‖y‖₊^2).

LaTeX

$$$\|x+y\|_+^2 + \|x-y\|_+^2 = 2(\|x\|_+^2 + \|y\|_+^2)$$$

Lean4

theorem parallelogram_law_with_nnnorm (x y : E) :
    ‖x + y‖₊ * ‖x + y‖₊ + ‖x - y‖₊ * ‖x - y‖₊ = 2 * (‖x‖₊ * ‖x‖₊ + ‖y‖₊ * ‖y‖₊) :=
  Subtype.ext <| parallelogram_law_with_norm 𝕜 x y

Похожие утверждения