const_add — Mathlib

English

If f is c-periodic, then the function x ↦ f(a + x) is c-periodic for any a.

Русский

Если f периодична по c, то функция x ↦ f(a + x) периодична по c для любого a.

LaTeX

$$$\\forall f:\\alpha→β, \\forall c:\\alpha, Periodic(f,c) ⇒ ∀ a:\\alpha, Periodic(x \\mapsto f(a+x), c)$$$

Lean4

theorem const_add [AddSemigroup α] (h : Periodic f c) (a : α) : Periodic (fun x => f (a + x)) c := fun x => by
  simpa [add_assoc] using h (a + x)

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