mem_cycleFactorsFinset_iff — Mathlib

English

A permutation p belongs to the cycle factors of f iff p is a cycle and p coincides with f on its support.

Русский

Перестановка p принадлежит факторным циклам f тогда и только тогда, когда p — цикл и p совпадает с f на опорном множестве.

LaTeX

$$$p \in cycleFactorsFinset(f) \\iff p.IsCycle \land \forall a \in p.support, p(a)=f(a)$$$

Lean4

theorem mem_cycleFactorsFinset_iff {f p : Perm α} : p ∈ cycleFactorsFinset f ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a :=
  by
  obtain ⟨l, hl, hl'⟩ := f.cycleFactorsFinset.exists_list_nodup_eq
  rw [← hl']
  rw [eq_comm, cycleFactorsFinset_eq_list_toFinset hl] at hl'
  simpa [List.mem_toFinset, Ne, ← hl'.right.right] using mem_list_cycles_iff hl'.left hl'.right.left

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