exists_mem_Ico — Mathlib

English

If f is periodic with positive period c in an ordered additive group, then for any x and a there exists y ∈ Ico a (a+c) with f(x) = f(y).

Русский

Если f периодична с положительным периодом c в линейно упорядоченной группе сложения, то для любых x и a найдется y ∈ Ico a (a+c) с f(x) = f(y).

LaTeX

$$$\text{Periodic}(f,c)\land 0

Lean4

/-- If a function `f` is `Periodic` with positive period `c`, then for all `x` there exists some
  `y ∈ Ico a (a + c)` such that `f x = f y`. -/
theorem exists_mem_Ico [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] (h : Periodic f c)
    (hc : 0 < c) (x a) : ∃ y ∈ Ico a (a + c), f x = f y :=
  let ⟨n, H, _⟩ := existsUnique_add_zsmul_mem_Ico hc x a
  ⟨x + n • c, H, (h.zsmul n x).symm⟩

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