nat_even_mul_periodic — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem nat_even_mul_periodic [NonAssocSemiring α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℕ) :
    Periodic f (n * (2 * c)) :=
  h.periodic_two_mul.nat_mul n

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