transnumAuxSeq_zero

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

URI: https://scilib.ai/kg/mathlib#CircleDeg1Lift.transnumAuxSeq_zero

English

For any f, the first term of the transnumAuxSeq equals f(0).

Русский

Для любого f первый член последовательности transnumAuxSeq равен f(0).

LaTeX

$$$ f.transnumAuxSeq(0) = f(0) $$$

Lean4

theorem transnumAuxSeq_zero : f.transnumAuxSeq 0 = f 0 := by simp [transnumAuxSeq]

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

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

Разделы

Аффилиация

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