lift_of_apply

Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra

URI: https://scilib.ai/kg/mathlib#FreeNonUnitalNonAssocAlgebra.lift_of_apply

English

lift_R f (of_R x) = f(x)

Русский

lift_R f (of_R x) = f(x)

LaTeX

$$$ lift\,R\ f (of\,R\ x) = f\,x. $$$

Lean4

@[simp]
theorem lift_of_apply (f : X → A) (x) : lift R f (of R x) = f x :=
  congr_fun (of_comp_lift _ f) x

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

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

Разделы

Аффилиация

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