English
Let f be periodic with period c > 0. Then the image of the half-open interval Ioc(a, a + c) under f coincides with the entire range of f, i.e., f[Ioc(a, a + c)] = range(f).
Русский
Пусть f периодична с периодом c > 0. Тогда образ полуширокого интервала Ioc(a, a + c) под действием f совпадает с множеством значений f, то есть f[Ioc(a, a + c)] = range(f).
LaTeX
$$$f[Ioc(a,a+c)] = \mathrm{range}(f)$$$
Lean4
theorem image_Ioc [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] (h : Periodic f c)
(hc : 0 < c) (a : α) : f '' Ioc a (a + c) = range f :=
(image_subset_range _ _).antisymm <|
range_subset_iff.2 fun x =>
let ⟨y, hy, hyx⟩ := h.exists_mem_Ioc hc x a
⟨y, hy, hyx.symm⟩
