vadd_apply — Mathlib

English

For any two continuous affine maps f: P →ᴬ[R] W and g: P →ᴬ[R] Q, and any p ∈ P, the action by vadd satisfies (f +ᵥ g)(p) = f(p) +ᵥ g(p).

Русский

Для любых двух непрерывных аффинных отображений f: P →ᴬ[R] W и g: P →ᴬ[R] Q и любого p ∈ P выполняется (f +ᵥ g)(p) = f(p) +ᵥ g(p).

LaTeX

$$$$(f +\\!_v g)(p) = f(p) +_v g(p).$$$$

Lean4

@[simp]
theorem vadd_apply (f : P →ᴬ[R] W) (g : P →ᴬ[R] Q) (p : P) : (f +ᵥ g) p = f p +ᵥ g p :=
  rfl

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