elim_of_mem — Mathlib

English

If hl guarantees that i :: l is nodup and hj is in l, then v.elim (mem_cons_of_mem _ hj) equals TProd.elim v.2 hj.

Русский

Если hl обеспечивает, что i :: l не повторяется, и hj ∈ l, тогда v.elim (mem_cons_of_mem _ hj) равно TProd.elim v.2 hj.

LaTeX

$$$v.elim (mem\\_cons\\_of\\_mem _ hj) = \\mathrm{TProd}.elim(v.2) hj$$$

Lean4

@[simp]
theorem elim_of_mem (hl : (i :: l).Nodup) (hj : j ∈ l) (v : TProd α (i :: l)) :
    v.elim (mem_cons_of_mem _ hj) = TProd.elim v.2 hj :=
  by
  apply elim_of_ne
  rintro rfl
  exact hl.notMem hj

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