neg — Mathlib

English

If f is antiperiodic with c, then f is antiperiodic with period −c.

Русский

Если f антипериодическая с периодом c, то она антипериодическая и с периодом −c.

LaTeX

$$$\text{Antiperiodic}(f,c) \rightarrow \text{Antiperiodic}(f,-c)$$$

Lean4

protected theorem neg [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) : Antiperiodic f (-c) := by
  simpa only [sub_eq_add_neg, Antiperiodic] using h.sub_eq

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