ofFun_mul — Mathlib

English

If f and g are ordinary functions from α to β, then their UniformFun embeddings multiply correspondingly: ofFun(f · g) = ofFun(f) · ofFun(g).

Русский

Если f и g — обычные функции α → β, то их отображения в UniformFun умножаются попарно: ofFun(f · g) = ofFun(f) · ofFun(g).

LaTeX

$$$\operatorname{ofFun}(f * g) = \operatorname{ofFun}(f) * \operatorname{ofFun}(g).$$$

Lean4

@[to_additive (attr := simp)]
theorem ofFun_mul [Mul β] (f g : α → β) : ofFun (f * g) = ofFun f * ofFun g :=
  rfl

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