nextOr_concat — Mathlib

English

If x is not in xs, then nextOr (xs ++ [x]) x d equals d.

Русский

Если x не принадлежит xs, то nextOr (xs ++ [x]) x d равно d.

LaTeX

$$$x\\notin xs\\Rightarrow nextOr(xs\\cup\\{x\\})\\ x\\ d= d$$$

Lean4

theorem nextOr_concat {xs : List α} {x : α} (d : α) (h : x ∉ xs) : nextOr (xs ++ [x]) x d = d := by
  induction xs with
  | nil => simp
  | cons z zs IH =>
    obtain ⟨hz, hzs⟩ := not_or.mp (mt mem_cons.2 h)
    rw [cons_append, nextOr_cons_of_ne _ _ _ _ hz, IH hzs]

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