duplicate_iff_sublist — Mathlib

English

x ∈+ l is equivalent to [x, x] being a sublist of l.

Русский

x дублируется в l тогда, когда [x, x] является подсписком l.

LaTeX

$$$ x \in+ l \iff [x, x] <+ l $$$

Lean4

/-- The contrapositive of `List.nodup_iff_sublist`. -/
theorem duplicate_iff_sublist : x ∈+ l ↔ [x, x] <+ l := by
  induction l with
  | nil => simp
  | cons y l IH =>
    by_cases hx : x = y
    · simp [hx, cons_sublist_cons, singleton_sublist]
    · rw [duplicate_cons_iff_of_ne hx, IH]
      refine ⟨sublist_cons_of_sublist y, fun h => ?_⟩
      cases h
      · assumption
      · contradiction

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