coeTree

Mathlib.Order.SuccPred.Tree

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

Lean4

/-- The coercion from a `SubRootedTree` to a `RootedTree`.
-/
@[coe, reducible]
noncomputable def coeTree {t : RootedTree} (r : SubRootedTree t) : RootedTree where α := Set.Ici r.root

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

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

Разделы

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

Аффилиация

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