const_sub

Mathlib.Algebra.Ring.Periodic

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

English

If f is c-periodic, then the function x ↦ f(a − x) is c-periodic.

Русский

Если f периодична по c, то функция x ↦ f(a − x) периодична по c.

LaTeX

$$$\\forall f:\\alpha→β, \\forall c:\\alpha, Periodic(f,c) ⇒ ∀ a:\\alpha, Periodic(x \\mapsto f(a-x), c)$$$

Lean4

theorem const_sub [AddCommGroup α] (h : Periodic f c) (a : α) : Periodic (fun x => f (a - x)) c := fun x => by
  simp only [← sub_sub, h.sub_eq]

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

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

Разделы

Аффилиация

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