treeHom_eq

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

URI: https://scilib.ai/kg/mathlib#IsFreeGroupoid.SpanningTree.treeHom_eq

← MathLib Explorer

English

For any path p in the spanning tree, treeHom T a equals homOfPath T p.

Русский

Для любого пути p в дерево-покрытии, дерево-образование равно homOfPath.

LaTeX

$$treeHom_eq$$

Lean4

/-- Any path to `a` gives `treeHom T a`, since paths in the tree are unique. -/
theorem treeHom_eq {a : G} (p : Path (root T) a) : treeHom T a = homOfPath T p := by rw [treeHom, Unique.default_eq]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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