nodup_flatten — Mathlib

English

The flattening of a list of lists is nodup iff every sublist is nodup and the sublists are pairwise disjoint.

Русский

Объединение (flatten) списка списков без повторов тогда и только тогда, когда каждый подсписок без повторов и подсписки попарно непересекаются.

LaTeX

$$$\\operatorname{Nodup}(\\operatorname{flatten} L) \\iff (\\forall l \\in L, \\operatorname{Nodup}(l)) \\land \\operatorname{Pairwise} \\operatorname{Disjoint} L$$$

Lean4

theorem nodup_flatten {L : List (List α)} : Nodup (flatten L) ↔ (∀ l ∈ L, Nodup l) ∧ Pairwise Disjoint L := by
  simp only [Nodup, pairwise_flatten, disjoint_left.symm, forall_mem_ne]

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