nodup_iff_sublist — Mathlib

English

A list l is nodup if and only if for every a, the list [a,a] is not a sublist of l.

Русский

Список l является нодуп тогда и только если для каждого a список [a,a] не является подсписком l.

LaTeX

$$$ \operatorname{Nodup}(l) \iff \forall a, \neg ([a,a] \sqsubset l) $$$

Lean4

theorem nodup_iff_sublist {l : List α} : Nodup l ↔ ∀ a, ¬[a, a] <+ l :=
  ⟨fun d a h => not_nodup_pair a (d.sublist h), by
    induction l <;> intro h; · exact nodup_nil
    case cons a l IH =>
      exact
        (IH fun a s => h a <| sublist_cons_of_sublist _ s).cons fun al => h a <| (singleton_sublist.2 al).cons_cons _⟩

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