snd_mk — Mathlib

English

The second projection of the constructed iterated product from a head i and tail l is the tail product, i.e., snd(List.TProd.mk(i :: l) f) = List.TProd.mk(l,f).

Русский

Вторая компонента List.TProd.mk(i :: l) f равна List.TProd.mk(l,f).

LaTeX

$$$\\mathrm{snd}(\\mathrm{List.TProd.mk}(i::l,f)) = \\mathrm{List.TProd.mk}(l,f).$$$

Lean4

@[simp]
theorem snd_mk (i : ι) (l : List ι) (f : ∀ i, α i) : (TProd.mk.{u, v} (i :: l) f).2 = TProd.mk.{u, v} l f :=
  rfl

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