nodup_sublists — Mathlib

English

The list of sublists has no duplicates if and only if the original list has no duplicates.

Русский

Подсписки не имеют повторов тогда и только тогда, когда исходный список не содержит повторов.

LaTeX

$$$\\operatorname{Nodup}(\\operatorname{sublists}(l)) \\iff \\operatorname{Nodup}(l)$$$

Lean4

@[simp]
theorem nodup_sublists {l : List α} : Nodup (sublists l) ↔ Nodup l :=
  ⟨fun h => (h.sublist (map_pure_sublist_sublists _)).of_map _, fun h =>
    (pairwise_sublists h).imp @fun l₁ l₂ h => by simpa using h.to_ne⟩

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