pow_comp — Mathlib

English

Let f: β → γ and g: α → β be continuous maps with γ a monoid with continuous multiplication. Then (f^n) ∘ g = (f ∘ g)^n for all n ∈ ℕ.

Русский

Пусть f: β → γ и g: α → β — непрерывные отображения, причём γ — моноид с непрерывным умножением. Тогда (f^n) ∘ g = (f ∘ g)^n для всех n ∈ ℕ.

LaTeX

$$$\forall f:\ C(\beta,\gamma),\ \forall n\in\mathbb{N},\ \forall g:\ C(\alpha,\beta): (f^n)\circ g = (f\circ g)^n.$$$

Lean4

@[to_additive]
theorem pow_comp [Monoid γ] [ContinuousMul γ] (f : C(β, γ)) (n : ℕ) (g : C(α, β)) : (f ^ n).comp g = f.comp g ^ n :=
  rfl

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