elim_self — Mathlib

English

For v ∈ List.TProd α (i :: l), the eliminator at the position mem_cons_self yields the first component, i.e., v.elim mem_cons_self = v.1.

Русский

Для v ∈ List.TProd α (i :: l) элиминация по mem_cons_self дает первую компоненту: v.elim mem_cons_self = v.1.

LaTeX

$$$(v\\,\\text{elim}\\ text{ mem\\_cons\\_self}) = v.\\mathrm{fst}.$$$

Lean4

@[simp]
theorem elim_self (v : TProd α (i :: l)) : v.elim mem_cons_self = v.1 := by simp [TProd.elim]

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