instMulUniformOnFun — Mathlib

English

For f,g in α →ᵤ[𝔖] β, the evaluation map toFun 𝔖 preserves multiplication: toFun 𝔖 (f * g) = toFun 𝔖 f * toFun 𝔖 g.

Русский

Для f,g ∈ α →ᵤ[𝔖] β отображение toFun 𝔖 сохраняет умножение: toFun 𝔖 (f * g) = toFun 𝔖 f * toFun 𝔖 g.

LaTeX

$$$\forall f,g : \alpha \to^u_{\mathfrak{S}} \beta,\; \operatorname{toFun}_{\mathfrak{S}}(f * g) = \operatorname{toFun}_{\mathfrak{S}}(f) * \operatorname{toFun}_{\mathfrak{S}}(g).$$$

Lean4

@[to_additive]
instance [Mul β] : Mul (α →ᵤ[𝔖] β) :=
  Pi.instMul

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