Path

Mathlib.Data.PFunctor.Multivariate.M

URI: https://scilib.ai/kg/mathlib#MvPFunctor.M.Path

Lean4

/-- A path from the root of a tree to one of its node -/
inductive Path : P.last.M → Fin2 n → Type u
  |
  root (x : P.last.M) (a : P.A) (f : P.last.B a → P.last.M) (h : PFunctor.M.dest x = ⟨a, f⟩) (i : Fin2 n)
    (c : P.drop.B a i) : M.Path x i
  |
  child (x : P.last.M) (a : P.A) (f : P.last.B a → P.last.M) (h : PFunctor.M.dest x = ⟨a, f⟩) (j : P.last.B a)
    (i : Fin2 n) (c : M.Path (f j) i) : M.Path x i

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

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

Разделы

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

Аффилиация

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