isCycleOn_inv — Mathlib

English

Taking inverse of a permutation preserves the cycle-on property on the same set.

Русский

Обратная перестановка сохраняет свойство цикла на заданном множестве.

LaTeX

$$$\\forall f : \\mathrm{Equiv.Perm}(\\alpha),\\; \\forall s : \\mathrm{Set}(\\alpha),\\; (f^{-1}).IsCycleOn s \\iff f.IsCycleOn s.$$$

Lean4

@[simp]
theorem isCycleOn_inv : f⁻¹.IsCycleOn s ↔ f.IsCycleOn s :=
  by
  simp only [IsCycleOn, sameCycle_inv, and_congr_left_iff]
  exact fun _ ↦ ⟨fun h ↦ Set.BijOn.perm_inv h, fun h ↦ Set.BijOn.perm_inv h⟩

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