iUnion_pnat_ptsOfPeriod — Mathlib

English

The same as above, using positive naturals: the union over all n in ℕ+ of ptsOfPeriod(f,n) equals periodicPts(f).

Русский

То же самое, но через положительные натуральные числа: объединение по всем n∈ℕ+ точек периода f равно periodicPts(f).

LaTeX

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

Lean4

theorem iUnion_pnat_ptsOfPeriod : ⋃ n : ℕ+, ptsOfPeriod f n = periodicPts f :=
  iSup_subtype.trans <| bUnion_ptsOfPeriod f

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