mk_get

Mathlib.Data.QPF.Multivariate.Constructions.Comp

URI: https://scilib.ai/kg/mathlib#MvQPF.Comp.mk_get

English

The operations mk and get are inverses: for any x, mk (get x) = x.

Русский

Операции mk и get являются обратными: для любого x, mk (get x) = x.

LaTeX

$$$\operatorname{Comp.mk}(\operatorname{Comp.get}(x)) = x.$$$

Lean4

@[simp]
protected theorem mk_get (x : Comp F G α) : Comp.mk (Comp.get x) = x :=
  rfl

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

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

Разделы

Аффилиация

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