add_antiperiod — Mathlib

English

If f is periodic with c1 and antiperiodic with c2, then f is antiperiodic with c1 + c2.

Русский

Если f периодична сдвигом c1 и антиперодична сдвигом c2, то f антиперiodична сдвигом c1 + c2.

LaTeX

$$$\forall x,\ f(x + (c_1 + c_2)) = -\,f(x)$$$

Lean4

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

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