sub_antiperiod_eq

Mathlib.Algebra.Ring.Periodic

URI: https://scilib.ai/kg/mathlib#Function.Periodic.sub_antiperiod_eq

← MathLib Explorer

English

If h1 is periodic with c1 and h2 is antiperiodic with c2, then f(c1 − c2) = − f(0).

Русский

Если f периодична с c1 и антиперiodична с c2, то f(c1 − c2) = − f(0).

LaTeX

$$$f(c_1 - c_2) = - f(0)$$$

Lean4

theorem sub_antiperiod_eq [AddGroup α] [InvolutiveNeg β] (h1 : Periodic f c₁) (h2 : Antiperiodic f c₂) :
    f (c₁ - c₂) = -f 0 :=
  (h1.sub_antiperiod h2).eq

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru