sub_period — Mathlib

English

If f is periodic with c1 and c2, then f is periodic with c1 − c2.

Русский

Если f периодична по c1 и по c2, то она периодична по c1 − c2.

LaTeX

$$$\\forall f:\\alpha→β, \\forall c_1,c_2:\\alpha, Periodic(f,c_1) ∧ Periodic(f,c_2) ⇒ Periodic(f(c_1−c_2))$$$

Lean4

theorem sub_period [AddGroup α] (h1 : Periodic f c₁) (h2 : Periodic f c₂) : Periodic f (c₁ - c₂) := fun x => by
  rw [sub_eq_add_neg, ← add_assoc, h2.neg, h1]

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