nodup — Mathlib

English

If a multiset of dependent pairs has pairwise distinct first components (NodupKeys), then the multiset is nodup.

Русский

Если мультимножество зависимых пар имеет попарно различные первые компоненты (NodupKeys), то мультимножество не имеет повторов (Nodup).

LaTeX

$$$$ \forall m : Multiset (\Sigma a, \beta a), \ m.NodupKeys \rightarrow m.Nodup $$$$

Lean4

protected theorem nodup {m : Multiset (Σ a, β a)} (h : m.NodupKeys) : m.Nodup :=
  h.nodup_keys.of_map _

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