mk_elim — Mathlib

English

If l is nodup and h is a way to recover an index from f, then TProd.mk l (v.elim' h) = v: the representation by mk is canonical.

Русский

Если l неповторимый и есть способ восстанавливания индекса из v, то TProd.mk l (v.elim' h) = v.

LaTeX

$$$\\text{mk\\_elim}(hnd, h, v):\\; \\mathrm{TProd.mk}\\; l\\ (v.\\elim' h) = v.$$$

Lean4

theorem mk_elim (hnd : l.Nodup) (h : ∀ i, i ∈ l) (v : TProd α l) : TProd.mk l (v.elim' h) = v :=
  TProd.ext hnd fun i hi => by simp [elim_mk]

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