int_odd_mul_antiperiodic — Mathlib

English

If f is antiperiodic with period c, then for any integer n the function f is antiperiodic with period n·(2c) + c, i.e. (2n+1)c.

Русский

Если f является антипериодической с периодом c, то для любого целого числа n функция f является антипериодической с периодом n·(2c) + c, то есть (2n+1)c.

LaTeX

$$$\text{Antiperiodic}(f,c) \rightarrow \forall n \in \mathbb{Z}, \ \text{Antiperiodic}(f,n\cdot(2c)+c)$$$

Lean4

theorem int_odd_mul_antiperiodic [NonAssocRing α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℤ) :
    Antiperiodic f (n * (2 * c) + c) := fun x => by rw [← add_assoc, h, h.int_even_mul_periodic]

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