eq_or_mem_of_mem_insertIdx — Mathlib

English

If a is in l.insertIdx n b, then either a = b or a ∈ l.

Русский

Если a ∈ l.insertIdx n b, то либо a = b, либо a ∈ l.

LaTeX

$$$a \\in l.insertIdx n b \\Rightarrow (a = b) \\lor (a \\in l)$$$

Lean4

theorem eq_or_mem_of_mem_insertIdx {l : List α} {n : ℕ} {a b : α} (h : a ∈ l.insertIdx n b) : a = b ∨ a ∈ l := by
  cases Nat.lt_or_ge (length l) n with
  | inl hn =>
    rw [insertIdx_of_length_lt hn] at h
    exact .inr h
  | inr hn => rwa [mem_insertIdx hn] at h

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