English
NodupKeys of a flattened list of lists corresponds to a pair: all embedded lists have NodupKeys and the disjointness of their key-collections.
Русский
NodupKeys у плоского списка списков эквивалентно: все вложенные списки имеют NodupKeys и множество ключей попарически непересекается.
LaTeX
$$$ \\mathrm{NodupKeys}(\\mathrm{flatten}(L)) \\iff \\Big( \\forall l \\in L,\\ \\mathrm{NodupKeys}(l) \\Big) \\land \\mathrm{Pairwise}\\mathrm{Disjoint}(L.map\\,\\mathrm{keys}) $$$
Lean4
theorem nodupKeys_flatten {L : List (List (Sigma β))} :
NodupKeys (flatten L) ↔ (∀ l ∈ L, NodupKeys l) ∧ Pairwise Disjoint (L.map keys) :=
by
rw [nodupKeys_iff_pairwise, pairwise_flatten, pairwise_map]
refine and_congr (forall₂_congr fun l _ => by simp [nodupKeys_iff_pairwise]) ?_
apply iff_of_eq; congr! with (l₁ l₂)
simp [keys, disjoint_iff_ne, Sigma.forall]
