toIcoMod_periodic — Mathlib

English

The locus of b with toIcoMod hp a b = toIocMod hp a b is the union over all integers z of the open intervals (a + z p, a + p + z p).

Русский

Место расположения таких b: toIcoMod hp a b = toIocMod hp a b образует объединение по z из интервалов (a + z p, a + p + z p).

LaTeX

$$$ \\{ b \\mid toIcoMod hp a b = toIocMod hp a b \\} = \\bigcup_{z \\in \\mathbb{Z}} \\mathrm{Ioo}(a + z p, a + p + z p) $$$

Lean4

theorem toIcoMod_periodic (a : α) : Function.Periodic (toIcoMod hp a) p :=
  toIcoMod_add_right hp a

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