add_period — Mathlib

English

If f is c-periodic, then f shifted by a is also c-periodic.

Русский

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

LaTeX

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

Lean4

theorem add_period [AddSemigroup α] (h1 : Periodic f c₁) (h2 : Periodic f c₂) : Periodic f (c₁ + c₂) := by
  simp_all [← add_assoc]

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