wPathDestRight_wPathCasesOn — Mathlib

English

Destructors on WPath provide left and right components: the left-dest maps to a drop of the path, the right-dest maps to a child path; together they reconstruct the original WPath via wPathCasesOn.

Русский

Разрушители WPath дают левый и правый компоненты: левый стартап сводится к drop-пути, правый к дочернему пути; вместе они восстанавливают исходный WPath через wPathCasesOn.

LaTeX

$$$n$-ary version of wPathDestLeft and wPathDestRight: for h, P.wPathCasesOn h g, we have wPathDestLeft (P.wPathCasesOn g' g) = g', wPathDestRight (P.wPathCasesOn g' g) = g.$$

Lean4

theorem wPathDestRight_wPathCasesOn {α : TypeVec n} {a : P.A} {f : P.last.B a → P.last.W} (g' : P.drop.B a ⟹ α)
    (g : ∀ j : P.last.B a, P.WPath (f j) ⟹ α) : P.wPathDestRight (P.wPathCasesOn g' g) = g :=
  rfl

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