add — Mathlib

English

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

Русский

Если f антипериодическая с периодами c1 и c2, то f периодична по сумме c1+c2.

LaTeX

$$$\text{Antiperiodic}(f,c_1) \rightarrow \text{Antiperiodic}(f,c_2) \rightarrow \text{Periodic}(f,c_1+c_2)$$$

Lean4

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

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