nodup_of_pairwise_disjoint_cycles

English

If l is a list of permutations such that every element is a cycle and the list elements are pairwise disjoint, then l has no duplicates.

Русский

Пусть l — список перестановок так, что каждый элемент является циклом, и элементы списка попарно непересекаются; тогда в списке нет повторяющихся элементов.

LaTeX

$$$\\forall \\beta, l : \\mathrm{List}(\\mathrm{Perm}(\\beta)),\\; (\\forall f \\in l, \\mathrm{IsCycle}(f)) \\land l.\\mathrm{Pairwise} \\mathrm{Disjoint} \\Rightarrow l.\\mathrm{Nodup}.$$$

Lean4

theorem nodup_of_pairwise_disjoint_cycles {l : List (Perm β)} (h1 : ∀ f ∈ l, IsCycle f) (h2 : l.Pairwise Disjoint) :
    l.Nodup :=
  nodup_of_pairwise_disjoint (fun h => (h1 1 h).ne_one rfl) h2

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