comp_wPathCasesOn — Mathlib

English

Composition with wPathCasesOn respects composition with h, i.e., applying h after wPathCasesOn equals wPathCasesOn after h, in a pointwise sense.

Русский

Составление с wPathCasesOn сохраняет композицию с h, т.е. применение h после wPathCasesOn равняется wPathCasesOn после h по точкам.

LaTeX

$$$\\forall {n} {P} {α β} (h : α \\Rightarrow β) {a} {f} {g'} {g} : h \\circ P.wPathCasesOn g' g = P.wPathCasesOn (h \\circ g') (\\lambda i. h \\circ g i)$$$

Lean4

theorem comp_wPathCasesOn {α β : TypeVec n} (h : α ⟹ β) {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) ⟹ α) : h ⊚ P.wPathCasesOn g' g = P.wPathCasesOn (h ⊚ g') fun i => h ⊚ g i := by
  ext i x; cases x <;> rfl

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