nodup_of_pairwise_disjoint — Mathlib

English

If a list l of permutations does not contain the identity and is pairwise disjoint, then l has no duplicates.

Русский

Если список перестановок не содержит единицу и попарно раздельен, то элементы списка различны.

LaTeX

$$$(1:\operatorname{Perm}(\alpha)) \notin l \;\land\; l.\mathrm{Pairwise} \operatorname{Disjoint} \Rightarrow l.\mathrm{Nodup}$$$

Lean4

theorem nodup_of_pairwise_disjoint {l : List (Perm α)} (h1 : (1 : Perm α) ∉ l) (h2 : l.Pairwise Disjoint) : l.Nodup :=
  by
  refine List.Pairwise.imp_of_mem ?_ h2
  intro τ σ h_mem _ h_disjoint _
  subst τ
  suffices (σ : Perm α) = 1 by
    rw [this] at h_mem
    exact h1 h_mem
  exact ext fun a => or_self_iff.mp (h_disjoint a)

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