dedup_eq_nil — Mathlib

English

Dedup(l) is the empty list if and only if l is the empty list.

Русский

Dedup(l) пустой список тогда и только тогда, когда l пустой.

LaTeX

$$$\\mathrm{dedup}(l) = [] \\iff l = []$$$

Lean4

@[simp]
theorem dedup_eq_nil (l : List α) : l.dedup = [] ↔ l = [] := by
  induction l with
  | nil => exact Iff.rfl
  | cons a l hl =>
    by_cases h : a ∈ l
    · simp only [List.dedup_cons_of_mem h, hl, List.ne_nil_of_mem h, reduceCtorEq]
    · simp only [List.dedup_cons_of_notMem h, List.cons_ne_nil]

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