English
Let f be periodic with c > 0. Then the image of the shifted interval uIcc(a, a + c) under f is the entire range of f, i.e., f[uIcc(a, a + c)] = range(f).
Русский
Пусть f периодична с периодом c > 0. Тогда образ смещенного интервала uIcc(a, a + c) под действием f равен всему диапазону значений f.
LaTeX
$$$f[uIcc(a,a+c)] = \mathrm{range}(f)$$$
Lean4
theorem image_uIcc [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] (h : Periodic f c)
(hc : c ≠ 0) (a : α) : f '' uIcc a (a + c) = range f := by
cases hc.lt_or_gt with
| inl hc =>
rw [uIcc_of_ge (add_le_of_nonpos_right hc.le), ← h.neg.image_Icc (neg_pos.2 hc) (a + c), add_neg_cancel_right]
| inr hc => rw [uIcc_of_le (le_add_of_nonneg_right hc.le), h.image_Icc hc]
