prod_snd_mk — Mathlib

English

Similarly, snd i (prod.mk i a b) = b for all i, with the result proven by induction on i.

Русский

Аналогично, snd i (prod.mk i a b) = b для любого i, доказательство идёт по индукции по i.

LaTeX

$$$\\mathrm{snd}(\\mathrm{prod.mk}\ i\ a\ b) = b$.$$

Lean4

@[simp]
theorem prod_snd_mk {α β : TypeVec n} (i : Fin2 n) (a : α i) (b : β i) : TypeVec.prod.snd i (prod.mk i a b) = b := by
  induction i with
  | fz => simp_all [prod.snd, prod.mk]
  | fs _ i_ih => apply i_ih

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