isPeriodicPt_iff_minimalPeriod_dvd

English

Two dynamical systems (f,x) and (g,y) have the same minimal period if and only if, for every n, x is periodic with period n under f exactly when y is periodic with period n under g.

Русский

Две динамические системы (f,x) и (g,y) имеют одинаковый минимальный период тогда и только тогда, когда для каждого n точка x периодична с периодом n по f тогда и только тогда, когда точка y периодична с периодом n по g.

LaTeX

$$$\\operatorname{minimalPeriod}(f,x) = \\operatorname{minimalPeriod}(g,y) \\iff \\forall n,\\ \\operatorname{IsPeriodicPt}(f,n,x) \\iff \\operatorname{IsPeriodicPt}(g,n,y)$$$

Lean4

theorem isPeriodicPt_iff_minimalPeriod_dvd : IsPeriodicPt f n x ↔ minimalPeriod f x ∣ n :=
  ⟨IsPeriodicPt.minimalPeriod_dvd, fun h => (isPeriodicPt_minimalPeriod f x).trans_dvd h⟩

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