comp — Mathlib

English

If f and g commute and x is periodic for f and for g with the same period n, then f ∘ g is periodic with period n at x.

Русский

Если f и g коммутируют и x периодично по f и по g с единым периодом n, то f ∘ g имеет период n в точке x.

LaTeX

$$%% The following reflects the formal statement: %%$$

Lean4

theorem comp {g : α → α} (hco : Commute f g) (hf : IsPeriodicPt f n x) (hg : IsPeriodicPt g n x) :
    IsPeriodicPt (f ∘ g) n x := by
  rw [IsPeriodicPt, hco.comp_iterate]
  exact IsFixedPt.comp hf hg

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