image_Icc — Mathlib

English

Let f be periodic with c > 0. Then f maps the closed interval Icc(a, a + c) onto the full range of f, i.e., f[Icc(a, a + c)] = range(f).

Русский

Пусть f периодична с периодом c > 0. Тогда образ замкнутого интервала Icc(a, a + c) при f совпадает с множеством значений f, т.е. f[Icc(a, a + c)] = range(f).

LaTeX

$$$f[Icc(a,a+c)] = \mathrm{range}(f)$$$

Lean4

theorem image_Icc [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] (h : Periodic f c)
    (hc : 0 < c) (a : α) : f '' Icc a (a + c) = range f :=
  (image_subset_range _ _).antisymm <| h.image_Ioc hc a ▸ image_mono Ioc_subset_Icc_self

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