mem_periodicPts — Mathlib

English

A point x is in the periodic points of f if and only if there exists a positive n with x being periodic of period n.

Русский

Точка x принадлежит к периодическим точкам f тогда и только тогда, когда существует положительный n, при котором x периодична с периодом n.

LaTeX

$$$$ x \\in \\operatorname{periodicPts}(f) \\;\\iff\\; \\exists n>0, \\text{IsPeriodicPt}(f,n,x). $$$$

Lean4

theorem mem_periodicPts : x ∈ periodicPts f ↔ ∃ n > 0, IsPeriodicPt f n x :=
  Iff.rfl

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