sub_const — Mathlib

English

Alternative formulation: if f is antiperiodic with c, then f(a − x) is antiperiodic with c for any a.

Русский

Альтернативная формулировка: если f антипериодическая с c, то f(a − x) антипериодична по c для любого a.

LaTeX

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

Lean4

theorem sub_const [SubtractionCommMonoid α] [Neg β] (h : Antiperiodic f c) (a : α) :
    Antiperiodic (fun x => f (x - a)) c := by simpa only [sub_eq_add_neg] using h.add_const (-a)

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