add_const — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem add_const [AddCommSemigroup α] (h : Periodic f c) (a : α) : Periodic (fun x => f (x + a)) c := fun x => by
  simpa only [add_right_comm] using h (x + a)

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