periodic — Mathlib

English

If a function is antiperiodic with antiperiod c, then it is periodic with period 2·c.

Русский

Если функция антипериодична с антипериодом c, то она периодична с периодом 2·c.

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 [AddMonoid α] [InvolutiveNeg β] (h : Antiperiodic f c) : Periodic f (2 • c) := by
  simp [two_nsmul, ← add_assoc, h _]

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