support_formPerm — Mathlib

English

The support of formPerm equals the attach of the cycle.

Русский

Опора formPerm равна распредлению (attach) цикла.

LaTeX

$$$\\operatorname{support}(s.formPerm) = s.toFinset$$$

Lean4

theorem support_formPerm [Fintype α] (s : Cycle α) (h : Nodup s) (hn : Nontrivial s) :
    support (formPerm s h) = s.toFinset := by
  obtain ⟨s⟩ := s
  refine support_formPerm_of_nodup s h ?_
  rintro _ rfl
  simpa [Nat.succ_le_succ_iff] using length_nontrivial hn

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