left_of_comp — Mathlib

English

If f and g commute and hfg: IsPeriodicPt (f ∘ g) n x and hg: IsPeriodicPt g n x, then IsPeriodicPt f n x.

Русский

Если f и g коммутируют и hfg: IsPeriodicPt (f ∘ g) n x и hg: IsPeriodicPt g n x, то IsPeriodicPt f n x.

LaTeX

$$%%$$

Lean4

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

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