directed_ptsOfPeriod_pnat — Mathlib

English

The family of sets of points of period n, as n ranges over positive naturals, is directed by inclusion: for any m,n ∈ ℕ+, there exists p = m·n such that ptsOfPeriod f m ⊆ ptsOfPeriod f p and ptsOfPeriod f n ⊆ ptsOfPeriod f p.

Русский

Семейство множеств периодических точек с периодом n, где n > 0, направлено включениями: для любых m,n > 0 существует p = m·n такое, что ptsOfPeriod f m ⊆ ptsOfPeriod f p и ptsOfPeriod f n ⊆ ptsOfPeriod f p.

LaTeX

$$$ \\text{Directed} \\ (\\mathrm{ptsOfPeriod}\\ f\\ n) \\text{ over } \\mathbb{N}_{>0} $ with witness p = m n.$$

Lean4

theorem directed_ptsOfPeriod_pnat (f : α → α) : Directed (· ⊆ ·) fun n : ℕ+ => ptsOfPeriod f n := fun m n =>
  ⟨m * n, fun _ hx => hx.mul_const n, fun _ hx => hx.const_mul m⟩

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