ext

Mathlib.Order.SuccPred.Tree

URI: https://scilib.ai/kg/mathlib#SubRootedTree.ext

English

Two subtrees of the same rooted tree are equal if their roots are equal.

Русский

Два поддерева одного корневого дерева равны, если их корни равны.

LaTeX

$${t : RootedTree} {v1 v2 : SubRootedTree t} (h : v1.root = v2.root) : v1 = v2$$

Lean4

@[ext]
theorem ext {t : RootedTree} {v₁ v₂ : SubRootedTree t} (h : v₁.root = v₂.root) : v₁ = v₂ :=
  h

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

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

Разделы

Аффилиация

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