mem_orderedInsert — Mathlib

English

For any a, b and l, a belongs to the list obtained by inserting b into l if and only if a = b or a belongs to l.

Русский

Для любых a, b и l, элемент a принадлежит списку, полученному после вставки b в l, тогда и только тогда, a = b или a принадлежит l.

LaTeX

$$$$ a \in \mathrm{orderedInsert}(r,b,l) \iff a = b \lor a \in l. $$$$

Lean4

@[simp]
theorem mem_orderedInsert {a b : α} {l : List α} : a ∈ orderedInsert r b l ↔ a = b ∨ a ∈ l :=
  match l with
  | [] => by simp [orderedInsert]
  | x :: xs => by
    rw [orderedInsert]
    split_ifs
    · simp
    · rw [mem_cons, mem_cons, mem_orderedInsert, or_left_comm]

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