elim_mk — Mathlib

English

For any nodup l and function f with i ∈ l, the elimination of the constructed mk(l,f) at i returns f(i): (List.TProd.mk l f).elim hi = f i.

Русский

Для неповторяющегося списка l и функции f при i ∈ l элиминация mk(l,f) даёт f(i).

LaTeX

$$$(\\mathrm{List.TProd.mk}\\; l\\; f).\\mathrm{elim} hi = f(i).$$$

Lean4

theorem elim_mk : ∀ (l : List ι) (f : ∀ i, α i) {i : ι} (hi : i ∈ l), (TProd.mk l f).elim hi = f i
  | i :: is, f, j, hj => by
    by_cases hji : j = i
    · subst hji
      simp
    · rw [TProd.elim_of_ne _ hji, snd_mk, elim_mk is]

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