of_subsingleton — Mathlib

English

Let α be a subsingleton type. For every function f: α → α, every n ∈ ℕ and every x ∈ α, x is a periodic point of f with period n.

Русский

Пусть α — одноэлементный тип. Для любой функции f: α → α, любого n ∈ ℕ и любого x ∈ α, x является периодической точкой функции f с периодом n.

LaTeX

$$$IsPeriodicPt(f,n,x) \Rightarrow f^{n}(x) = x$$$

Lean4

@[nontriviality]
theorem of_subsingleton [Subsingleton α] (f : α → α) (n : ℕ) (x : α) : IsPeriodicPt f n x :=
  IsFixedPt.of_subsingleton _ _

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