English
Let f: α → β be periodic with a positive period c on an ordered additive group α. For every x ∈ α and a ∈ α there exists y ∈ Ioc(a, a + c) such that f(x) = f(y).
Русский
Пусть f: α → β периодична с положительным периодом c на упорядоченной аддитивной группе α. Для любых x ∈ α и a ∈ α существует y ∈ Ioc(a, a + c) такое, что f(x) = f(y).
LaTeX
$$$\forall x\,\forall a,\exists y\in Ioc(a,a+c),\ f(x)=f(y)$$$
Lean4
/-- If a function `f` is `Periodic` with positive period `c`, then for all `x` there exists some
`y ∈ Ioc a (a + c)` such that `f x = f y`. -/
theorem exists_mem_Ioc [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] (h : Periodic f c)
(hc : 0 < c) (x a) : ∃ y ∈ Ioc a (a + c), f x = f y :=
let ⟨n, H, _⟩ := existsUnique_add_zsmul_mem_Ioc hc x a
⟨x + n • c, H, (h.zsmul n x).symm⟩
