get_mk

Mathlib.Data.QPF.Multivariate.Constructions.Comp

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

English

Again, the destruct and make operations are inverse: get (mk x) = x for x in the appropriate type.

Русский

Снова: деструктор и конструктор взаимно обратны: get (mk x) = x.

LaTeX

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

Lean4

@[simp]
protected theorem get_mk (x : F fun i ↦ G i α) : Comp.get (Comp.mk x) = x :=
  rfl

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

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

Разделы

Аффилиация

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