add_const — Mathlib

English

If f is antiperiodic with c, then the function x ↦ f(a + x) is also antiperiodic with period c, for any a.

Русский

Если f антипериодическая с c, то функция x ↦ f(a + x) также антипериодична по периоду c для любого a.

LaTeX

$$$\forall a, \text{Antiperiodic}(f,c) \rightarrow \text{Antiperiodic}(f( a + x ), c)$$$

Lean4

theorem add_const [AddCommSemigroup α] [Neg β] (h : Antiperiodic f c) (a : α) : Antiperiodic (fun x => f (x + a)) c :=
  fun x => by simpa only [add_right_comm] using h (x + a)

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