prev_cons_cons_eq' — Mathlib

English

For l, y, z with hxy, if x ∈ y :: z :: l and hx: x = y, then prev (y :: z :: l) x h = getLast (z :: l) (cons_ne_nil _ _).

Русский

Для l, y, z с hxy, если x ∈ y :: z :: l и hx: x = y, тогда prev (y :: z :: l) x h = getLast (z :: l).

LaTeX

$$$Prev\\ (y::z::l)\\ x\\ h = getLast(z::l)\\ (cons\\_ne\\_nil\\ _\\ _)$$$

Lean4

theorem prev_cons_cons_eq' (y z : α) (h : x ∈ y :: z :: l) (hx : x = y) :
    prev (y :: z :: l) x h = getLast (z :: l) (cons_ne_nil _ _) := by rw [prev, dif_pos hx]

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