toFun_mul — Mathlib

English

Let f and g be elements of UniformFun α β, where β is equipped with a multiplication. Then the underlying function respects multiplication, i.e. the evaluation map commutes with the product: toFun(f · g) = toFun(f) · toFun(g).

Русский

Пусть f и g — элементы UniformFun α β, где β имеет умножение. Тогда проекция на базовое множество сохраняет умножение: toFun(f · g) = toFun(f) · toFun(g).

LaTeX

$$$\forall f,g \in \alpha \to^u \beta,\; \operatorname{toFun}(f * g) = \operatorname{toFun}(f) * \operatorname{toFun}(g).$$$

Lean4

@[to_additive (attr := simp)]
theorem toFun_mul [Mul β] (f g : α →ᵤ β) : toFun (f * g) = toFun f * toFun g :=
  rfl

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