wMk — Mathlib

English

Eta equation for the right destructor: applying the wPathCasesOn to the path yields the right projection matching g.

Русский

Эта η-лемма на правый деструктор: применение wPathCasesOn к пути даёт правый проектор, совпадающий с g.

LaTeX

$$$wPathDestRight_wPathCasesOn {\alpha} {a} {f} (g' : P.drop.B a ⟹ α) (g : ∀ j, P.WPath (f j) ⟹ α) : P.wPathDestRight (P.wPathCasesOn g' g) = g$$

Lean4

/-- Constructor for `W` -/
def wMk {α : TypeVec n} (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α) : P.W α :=
  let g : P.last.B a → P.last.W := fun i => (f i).fst
  let g' : P.WPath ⟨a, g⟩ ⟹ α := P.wPathCasesOn f' fun i => (f i).snd
  ⟨⟨a, g⟩, g'⟩

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