funext — Mathlib

English

If f is antiperiodic with antiperiod c, then the function shifted by c equals the negation of f; i.e., f(x+c) = −f(x) for all x.

Русский

Если функция f антипериодична с антипериодом c, тогда сдвиг функции на c равен противоположности f; то есть f(x+c) = −f(x) для всех x.

LaTeX

$$$[Add\ α][Neg\ β]\ (h:Antiperiodic\ f\ c)\Rightarrow(\forall x:\alpha,\ f(x+c) = -f(x)).$$$

Lean4

protected theorem funext [Add α] [Neg β] (h : Antiperiodic f c) : (fun x => f (x + c)) = -f :=
  funext h

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