existsUnique_cycle_subtype — Mathlib

English

Let α be a finite type and f a cyclic permutation of α. Then there exists a unique cycle s with Nodup such that the associated permutation of s equals f.

Русский

Пусть α конечен и f—цикл в группе перестановок α. Тогда существует единственный цикл s с свойством Nodup, чья сопряженная перестановка равна f.

LaTeX

$$$\\\\exists! s : { s : Cycle\\\\ α // s.Nodup }, (s : Cycle α).formPerm s.prop = f$$$

Lean4

theorem existsUnique_cycle_subtype {f : Perm α} (hf : IsCycle f) :
    ∃! s : { s : Cycle α // s.Nodup }, (s : Cycle α).formPerm s.prop = f :=
  by
  obtain ⟨s, ⟨hs, rfl⟩, hs'⟩ := hf.existsUnique_cycle
  refine ⟨⟨s, hs⟩, rfl, ?_⟩
  rintro ⟨t, ht⟩ ht'
  simpa using hs' _ ⟨ht, ht'⟩

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