mul_apply

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

English

For all f,g and x, (f * g) x = f (g x).

Русский

Для любых f,g и x выполняется (f*g) x = f(g(x)).

LaTeX

$$$\\forall f,g \\in CircleDeg1Lift,\\forall x \\in \\mathbb{R},\\ (f*g)(x)=f(g(x))$$$

Lean4

theorem mul_apply (x) : (f * g) x = f (g x) :=
  rfl

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

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

Разделы

Аффилиация

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