get_mk

Mathlib.Data.PFunctor.Multivariate.Basic

URI: https://scilib.ai/kg/mathlib#MvPFunctor.comp.get_mk

English

The construction comp.mk is a right-inverse of comp.get; applying comp.get to comp.mk x returns x.

Русский

Операция comp.mk является правая обратная операции comp.get: применив comp.get к comp.mk x, получаем x.

LaTeX

$$$\\operatorname{comp.get}\\bigl( \\operatorname{comp.mk} x \\bigr) = x$$$

Lean4

@[simp]
theorem get_mk (x : P (fun i => Q i α)) : comp.get (comp.mk x) = x := by rfl

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

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

Разделы

Аффилиация

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