periodic_with_period_zero

Mathlib.Algebra.Ring.Periodic

URI: https://scilib.ai/kg/mathlib#Function.periodic_with_period_zero

English

Every function is periodic with period 0; i.e., f(x+0) = f(x) for all x.

Русский

Любая функция имеет период 0; то есть f(x+0) = f(x) для всех x.

LaTeX

$$$\forall f:\alpha\to \beta,\ Periodic\ f\ 0.$$$

Lean4

theorem periodic_with_period_zero [AddZeroClass α] (f : α → β) : Periodic f 0 := fun x => by rw [add_zero]

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

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

Разделы

Аффилиация

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