mul_comp — Mathlib

English

The product of two continuous maps composed with g equals the product of the compositions: (f1 · f2) ∘ g = (f1 ∘ g) · (f2 ∘ g).

Русский

Произведение двух отображений, закомпонованное с g, равно произведению их композиций: (f1 · f2) ∘ g = (f1 ∘ g) · (f2 ∘ g).

LaTeX

$$ (f1 * f2).comp g = f1.comp g * f2.comp g $$

Lean4

@[to_additive (attr := simp)]
theorem mul_comp [Mul γ] [ContinuousMul γ] (f₁ f₂ : C(β, γ)) (g : C(α, β)) : (f₁ * f₂).comp g = f₁.comp g * f₂.comp g :=
  rfl

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