funext — Mathlib

English

If f is periodic with period c in an additive domain, then for all x, f(x+c) = f(x).

Русский

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

LaTeX

$$$\\forall \\alpha,\\beta,\\gamma,\, f:\\alpha\\to\\beta,\\ c:\\alpha,\\[Add\\alpha]\\, \\mathrm{Periodic}(f,c) \\Rightarrow (fun x \\to f(x+c)) = f.$$$

Lean4

protected theorem funext [Add α] (h : Periodic f c) : (fun x => f (x + c)) = f :=
  funext h

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