wMk_eq — Mathlib

English

The W-constructor wMk is compatible with the internal decomposition: wMk a g' (i ↦ ⟨f i, g i⟩) equals the pair (a, f) with the path data given by g.

Русский

Конструктор W-пусть wMk совместим с внутренним разложением: wMk a g' (i ↦ ⟨f i, g i⟩) равняется паре (a, f) с данными пути, заданными g.

LaTeX

$$$ (P.wMk\ a\ g'\ (\lambda i.\langle f(i), g(i)\rangle)) = (\langle\langle a, f\rangle, P.wPathCasesOn\ g'\ g\rangle).$$$

Lean4

theorem wMk_eq {α : 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.wMk a g' fun i => ⟨f i, g i⟩) = ⟨⟨a, f⟩, P.wPathCasesOn g' g⟩ :=
  rfl

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