pathDestRight — Mathlib

English

From a destination and a path, extract a right-branch arrow into α parameterized by j.

Русский

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

LaTeX

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

Lean4

/-- Implementation of destructor for M-type of `P` -/
def pathDestRight {α : 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 ⟹ α) : ∀ j : P.last.B a, M.Path P (f j) ⟹ α := fun j i c => f' i (M.Path.child x a f h j i c)

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