liftOn_mk

Mathlib.GroupTheory.MonoidLocalization.Basic

URI: https://scilib.ai/kg/mathlib#Localization.liftOn_mk

English

The liftOn value on a canonical mk a b equals f a b.

Русский

Значение liftOn на каноническом mk a b равно f a b.

LaTeX

$$$ liftOn\ (mk a b)\ f\ H = f a b $$$

Lean4

@[to_additive]
theorem liftOn_mk {p : Sort u} (f : M → S → p) (H) (a : M) (b : S) : liftOn (mk a b) f H = f a b :=
  rfl

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

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

Разделы

Аффилиация

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