pathDestLeft — Mathlib

English

From a destination and a path, extract a left-branch arrow into α by applying f' to the root path.

Русский

Из назначения и пути извлекаем левый разветвляющий стрелок в α через применение f' к корневому пути.

LaTeX

$$$\\text{pathDestLeft} : (h : PFunctor.M.dest x = ⟨a,f⟩) \\to (f' : M.Path P x \\Rightarrow α) \\to P.drop.B a \\Rightarrow α$$$

Lean4

/-- Implementation of destructor for M-type of `P` -/
def pathDestLeft {α : TypeVec n} {x : P.last.M} {a : P.A} {f : P.last.B a → P.last.M} (h : PFunctor.M.dest x = ⟨a, f⟩)
    (f' : M.Path P x ⟹ α) : P.drop.B a ⟹ α := fun i c => f' i (M.Path.root x a f h i c)

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