existsUnique_cycle_nontrivial_subtype

English

If f is a cycle, there exists a unique s in the set of cycles with Nodup and Nontrivial such that the left component of s corresponds to f via the formPerm map.

Русский

Пусть f—цикл. Тогда существует единственный s в множество циклов с Nodup и Nontrivial such that s через формуPerm соответствуют f.

LaTeX

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

Lean4

theorem existsUnique_cycle_nontrivial_subtype {f : Perm α} (hf : IsCycle f) :
    ∃! s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }, (s : Cycle α).formPerm s.prop.left = f :=
  by
  obtain ⟨⟨s, hn⟩, hs, hs'⟩ := hf.existsUnique_cycle_subtype
  refine ⟨⟨s, hn, ?_⟩, ?_, ?_⟩
  · rw [hn.nontrivial_iff]
    subst f
    intro H
    refine hf.ne_one ?_
    simpa using Cycle.formPerm_subsingleton _ H
  · simpa using hs
  · rintro ⟨t, ht, ht'⟩ ht''
    simpa using hs' ⟨t, ht⟩ ht''

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