nodup_sublistsLen — Mathlib

English

If l is Nodup, then for every n, the list sublistsLen n l has no duplicates.

Русский

Если l без повторов, то для каждого n подспискиLen n l не повторяются.

LaTeX

$$$\\forall n:\\, \\mathbb{N},\\ operatorname{Nodup}(l) \\Rightarrow \\operatorname{Nodup}(\\operatorname{sublistsLen}(n, l))$$$

Lean4

theorem nodup_sublistsLen (n : ℕ) {l : List α} (h : Nodup l) : (sublistsLen n l).Nodup :=
  by
  have : Pairwise (· ≠ ·) l.sublists' :=
    Pairwise.imp (fun h => Lex.to_ne (by convert h using 3; simp [eq_comm])) h.sublists'
  exact this.sublist (sublistsLen_sublist_sublists' _ _)

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