add_apply — Mathlib

English

Let f,g ∈ C_c(α,β). If β has an additive structure with a zero and the addition is continuous, then C_c(α,β) inherits pointwise addition: (f+g)(x) = f(x) + g(x) for every x ∈ α.

Русский

Пусть f,g ∈ C_c(α,β). Если β имеет аддитивную структуру с нулём и сумма непрерывна, то C_c(α,β) наследует сумму по точкам: (f+g)(x) = f(x) + g(x) для каждого x ∈ α.

LaTeX

$$$\forall f,g \in C_c(\alpha,\beta), \forall x \in \alpha, \ (f+g)(x) = f(x) + g(x)$$$

Lean4

theorem add_apply [AddZeroClass β] [ContinuousAdd β] (f g : C_c(α, β)) : (f + g) x = f x + g x :=
  rfl

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