sub — Mathlib

English

Let α be an additive group and β a type with negation. For f: α → β, if f is antiperiodic with shifts c1 and c2, then f is periodic with shift c1 − c2.

Русский

Пусть α — аддитивная группа, β — множество с операцией отрицания. Пусть f: α → β. Если f антиперiodична сдвигами c1 и c2, то f периодична сдвигом c1 − c2.

LaTeX

$$$\forall x,\ f(x + (c_1 - c_2)) = f(x)$$$

Lean4

theorem sub [AddGroup α] [InvolutiveNeg β] (h1 : Antiperiodic f c₁) (h2 : Antiperiodic f c₂) : Periodic f (c₁ - c₂) :=
  by simpa only [sub_eq_add_neg] using h1.add h2.neg

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