wPathCasesOn_eta — Mathlib

English

The wPathCasesOn construction is an inverse to the wPathDestLeft and wPathDestRight destructors: applying wPathCasesOn to the left and right components recovers the original WPath.

Русский

Конструкция wPathCasesOn обратна деструкторам wPathDestLeft и wPathDestRight: применение к левой и правой составляющим восстанавливает исходный WPath.

LaTeX

$$$\forall {n} (P) {\alpha} {a} {f} (h) : P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) = h$$$

Lean4

theorem wPathCasesOn_eta {α : TypeVec n} {a : P.A} {f : P.last.B a → P.last.W} (h : P.WPath ⟨a, f⟩ ⟹ α) :
    P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) = h := by ext i x; cases x <;> rfl

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