add_apply — Mathlib

English

Let p and q be seminorms on a vector space E over 𝕜. Then their pointwise sum is again a seminorm, and for every x ∈ E one has (p + q)(x) = p(x) + q(x).

Русский

Пусть p и q — полунормы на векторном пространстве E над 𝕜. Тогда их точечная сумма является полунормой и для каждого x ∈ E выполняется (p + q)(x) = p(x) + q(x).

LaTeX

$$$ (p+q)(x) = p(x) + q(x) $$$

Lean4

@[simp]
theorem add_apply (p q : Seminorm 𝕜 E) (x : E) : (p + q) x = p x + q x :=
  rfl

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