mem_ptsOfPeriod

Mathlib.Dynamics.PeriodicPts.Defs

URI: https://scilib.ai/kg/mathlib#Function.mem_ptsOfPeriod

English

x ∈ ptsOfPeriod f n iff IsPeriodicPt f n x.

Русский

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

LaTeX

$$$x \in ptsOfPeriod(f,n) \iff IsPeriodicPt(f,n,x)$$$

Lean4

@[simp]
theorem mem_ptsOfPeriod : x ∈ ptsOfPeriod f n ↔ IsPeriodicPt f n x :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru