odd_zsmul_antiperiodic — Mathlib

English

Let α be an additive group and β a type with an involutive negation. If f is antiperiodic with period c, then for every integer n the function f is antiperiodic with period (2n+1)·c.

Русский

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

LaTeX

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

Lean4

theorem odd_zsmul_antiperiodic [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℤ) :
    Antiperiodic f ((2 * n + 1) • c) := by
  intro x
  rw [add_zsmul, one_zsmul, ← add_assoc, h, h.even_zsmul_periodic]

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