exists_cycleOn — Mathlib

English

Every finite set s admits a cycle f with support contained in s and f.IsCycleOn s.

Русский

Каждое конечное множество s допускает цикл f с опорой внутри s и IsCycleOn s.

LaTeX

$$$\exists f\in\mathrm{Perm}(\alpha), f.IsCycleOn(s) \land \mathrm{supp}(f) \subseteq s$$$

Lean4

theorem exists_cycleOn (s : Finset α) : ∃ f : Perm α, f.IsCycleOn s ∧ f.support ⊆ s :=
  by
  refine ⟨s.toList.formPerm, ?_, fun x hx => by simpa using List.mem_of_formPerm_apply_ne (Perm.mem_support.1 hx)⟩
  convert s.nodup_toList.isCycleOn_formPerm
  simp

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