periodic_two_mul — Mathlib

English

If an antiperiodic f with c is given, then f has period 2·c; equivalently, f(x+2c)=f(x) for all x.

Русский

Если задана антипериодичность f с c, тогда f имеет период 2·c; то есть f(x+2c)=f(x) для всех x.

LaTeX

$$$\forall f\,c, Antiperiodic\ f\ c \Rightarrow Periodic\ f\ (2\cdot c).$$$

Lean4

/-- If a function is `antiperiodic` with antiperiod `c`, then it is also `Periodic` with period
  `2 * c`. -/
protected theorem periodic_two_mul [NonAssocSemiring α] [InvolutiveNeg β] (h : Antiperiodic f c) : Periodic f (2 * c) :=
  nsmul_eq_mul 2 c ▸ h.periodic

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