nodup_sublists' — Mathlib

English

The nodup property for sublists' is equivalent to the nodup property for the original list.

Русский

Свойство Nodup для подсписков' эквивалентно свойству Nodup исходного списка.

LaTeX

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

Lean4

@[simp]
theorem nodup_sublists' {l : List α} : Nodup (sublists' l) ↔ Nodup l := by
  rw [sublists'_eq_sublists, nodup_map_iff reverse_injective, nodup_sublists, nodup_reverse]

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