fst_prod_mk — Mathlib

English

Theorem: TypeVec.prod.fst ∘ (prod.map f g) = f ∘ TypeVec.prod.fst, i.e., taking the first projection after mapping corresponds to mapping the first projection.

Русский

Теорема: TypeVec.prod.fst ∘ (prod.map f g) = f ∘ TypeVec.prod.fst, то есть взяв первую проекцию после отображения, получаем отображение первой проекции.

LaTeX

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

Lean4

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

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