minimalPeriod_pos_iff_mem_periodicPts

English

The union over positive natural numbers of ptsOfPeriod equals periodicPts f.

Русский

Объединение по всем n ∈ ℕ+ точек периода равно периодическим точкам f.

LaTeX

$$$$ \\bigcup_{n \\in \\mathbb{N}_{>0}} \\operatorname{ptsOfPeriod}(f,n) = \\operatorname{periodicPts}(f). $$$$

Lean4

theorem minimalPeriod_pos_iff_mem_periodicPts : 0 < minimalPeriod f x ↔ x ∈ periodicPts f :=
  ⟨not_imp_not.1 fun h => by simp only [minimalPeriod, dif_neg h, lt_irrefl 0, not_false_iff],
    minimalPeriod_pos_of_mem_periodicPts⟩

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