const_mul — Mathlib

English

If f is antiperiodic with c, then for every a ≠ 0 the function x ↦ f(a • x) is antiperiodic with period a⁻¹ • c.

Русский

Если f антипериодична с периодом c, то для любого a ≠ 0 функция x ↦ f(a • x) антипериодична с периодом a⁻¹ • c.

LaTeX

$$$\text{Antiperiodic}(f(a\cdot), a^{-1} c)$ for all $a \neq 0$$$

Lean4

theorem const_mul [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α} (ha : a ≠ 0) :
    Antiperiodic (fun x => f (a * x)) (a⁻¹ * c) :=
  h.const_smul₀ ha

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