ne_singleton_iff — Mathlib

English

For any list l and element x, l ≠ [x] iff l = [] or ∃ y ∈ l with y ≠ x.

Русский

Для любого списка l и элемента x, l ≠ [x] тогда и только тогда, когда l = [] или существует y ∈ l и y ≠ x.

LaTeX

$$$ l \neq [x] \iff l = [] \lor \exists y \in l, y \neq x $$$

Lean4

theorem ne_singleton_iff {l : List α} (h : Nodup l) (x : α) : l ≠ [x] ↔ l = [] ∨ ∃ y ∈ l, y ≠ x := by
  induction l with
  | nil => simp
  | cons hd tl hl =>
    specialize hl h.of_cons
    by_cases hx : tl = [x]
    · simpa [hx, and_comm, and_or_left] using h
    · rw [← Ne, hl] at hx
      rcases hx with (rfl | ⟨y, hy, hx⟩)
      · simp
      · suffices ∃ y ∈ hd :: tl, y ≠ x by simpa [ne_nil_of_mem hy]
        exact ⟨y, mem_cons_of_mem _ hy, hx⟩

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