sub_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 sub_antiperiod [AddGroup α] [InvolutiveNeg β] (h1 : Periodic f c₁) (h2 : Antiperiodic f c₂) :
    Antiperiodic f (c₁ - c₂) := by simpa only [sub_eq_add_neg] using h1.add_antiperiod h2.neg

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