ofFun_mul — Mathlib

English

If f,g are ordinary functions α → β, then their UniformOnFun embeddings multiply pointwise: ofFun 𝔖 (f * g) = ofFun 𝔖 f * ofFun 𝔖 g.

Русский

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

LaTeX

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

Lean4

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

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