snd_prod_mk — Mathlib

English

Similarly, TypeVec.prod.snd ∘ (prod.map f g) = g ∘ TypeVec.prod.snd; the second projection commutes with the product map.

Русский

Аналогично, TypeVec.prod.snd ∘ (prod.map f g) = g ∘ TypeVec.prod.snd; вторичная проекция коммутирует с отображением произведения.

LaTeX

$$$\\mathrm{snd} \\circ (\\mathrm{prod.map}\ f\ g) = g \\circ \\mathrm{snd}$$$

Lean4

theorem snd_prod_mk {α α' β β' : TypeVec n} (f : α ⟹ β) (g : α' ⟹ β') :
    TypeVec.prod.snd ⊚ (f ⊗' g) = g ⊚ TypeVec.prod.snd := by funext i;
  induction i with
  | fz => rfl
  | fs _ i_ih => apply i_ih

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