mul_apply

Mathlib.Algebra.Group.End

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.mul_apply

English

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

Русский

Для любых f,g ∈ Perm α и x ∈ α, (f * g) x = f (g x).

LaTeX

$$$\\\\forall f,g \\\\in \\\\operatorname{Perm}(\\\\alpha), \\\\forall x \\\\in \\\\alpha, \\\\ (f * g) x = f (g x)$$$

Lean4

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

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

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

Разделы

Аффилиация

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