ext_mk

Mathlib.Data.QPF.Multivariate.Constructions.Cofix

URI: https://scilib.ai/kg/mathlib#MvQPF.Cofix.ext_mk

English

Extensionality with mk: equality of mk-images implies equality of images.

Русский

Экстенсиональность через mk: равенство mk x и mk y имплицирует равенство x и y.

LaTeX

$$$\\forall x y,\\; \\mathrm{Cofix.mk} x = \\mathrm{Cofix.mk} y \\Rightarrow x=y$$$

Lean4

theorem ext_mk {α : TypeVec n} (x y : F (α ::: Cofix F α)) (h : Cofix.mk x = Cofix.mk y) : x = y := by
  rw [← Cofix.dest_mk x, h, Cofix.dest_mk]

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

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

Разделы

Аффилиация

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