exists_mem_Ico₀ — Mathlib

English

If f is periodic with period c > 0 in an Archimedean ordered group, then for every x there exists some y ∈ Ico 0 c with f(x) = f(y).

Русский

Если f периодична с периодом c > 0 в упорядоченной группе Архимеда, то для каждого x существует y ∈ Ico 0 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 0 c` such that `f x = f y`. -/
theorem exists_mem_Ico₀ [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] (h : Periodic f c)
    (hc : 0 < c) (x) : ∃ y ∈ Ico 0 c, f x = f y :=
  let ⟨n, H, _⟩ := existsUnique_zsmul_near_of_pos' hc x
  ⟨x - n • c, H, (h.sub_zsmul_eq n).symm⟩

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