eq_or_ne_mem_of_mem — Mathlib

English

Given a ∈ b :: l, either a = b or (a ≠ b and a ∈ l).

Русский

Если a принадлежит b :: l, то либо a = b, либо (a ≠ b и a ∈ l).

LaTeX

$$a ∈ List.cons b l → (a = b) ∨ (a ≠ b ∧ a ∈ l)$$

Lean4

theorem _root_.Decidable.List.eq_or_ne_mem_of_mem [DecidableEq α] {a b : α} {l : List α} (h : a ∈ b :: l) :
    a = b ∨ a ≠ b ∧ a ∈ l := by
  by_cases hab : a = b
  · exact Or.inl hab
  · exact ((List.mem_cons.1 h).elim Or.inl (fun h => Or.inr ⟨hab, h⟩))

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