mul_apply — Mathlib

English

The product of two continuous maps evaluated at a point x is the product of their values at x.

Русский

Произведение двух непрерывных отображений в точке x равно произведению их значений в точке x.

LaTeX

$$For f,g ∈ C(α, β) and x ∈ α, (f * g)(x) = f(x) · g(x).$$

Lean4

@[to_additive (attr := simp)]
theorem mul_apply [Mul β] [ContinuousMul β] (f g : C(α, β)) (x : α) : (f * g) x = f x * g x :=
  rfl

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