ext

Mathlib.Data.QPF.Multivariate.Constructions.Cofix

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

English

Extensionality for Cofix: two Cofix elements are equal if their destinations are equal.

Русский

Экстенсиональность Cofix: два элемента Cofix равны, если их dest равны.

LaTeX

$$$\\forall x y,\\; x.d est = y.dest \\Rightarrow x=y$$$

Lean4

theorem ext {α : TypeVec n} (x y : Cofix F α) (h : x.dest = y.dest) : x = y := by
  rw [← Cofix.mk_dest x, h, Cofix.mk_dest]

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

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

Разделы

Аффилиация

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