int_even_mul_periodic — Mathlib

English

If f is antiperiodic with c in a NonAssocRing α and β has involutive negation, then f is periodic with period n*(2*c) for any integer n.

Русский

Если f антипериодична с c в NonAssocRing α и β имеет инволютивное отрицание, то f периодична с периодом n*(2*c) для любого целого n.

LaTeX

$$$[NonAssocRing\ α][InvolutiveNeg\ β]\Rightarrow(\forall h:Antiperiodic\ f\ c)(\forall n\in \mathbb{Z})\, Periodic\ f\ (n\cdot (2\cdot c)).$$$

Lean4

theorem int_even_mul_periodic [NonAssocRing α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℤ) :
    Periodic f (n * (2 * c)) :=
  h.periodic_two_mul.int_mul n

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