cycleFactorsFinset_eq_singleton_iff

English

For any f,g, cycleFactorsFinset f = {g} iff f.IsCycle ∧ f = g.

Русский

Для любых f,g: cycleFactorsFinset f = {g} эквивалентно f.IsCycle и f = g.

LaTeX

$$$\forall {f,g}: cycleFactorsFinset(f) = {g} \iff f.IsCycle \land f = g$$$

Lean4

theorem cycleFactorsFinset_eq_singleton_iff {f g : Perm α} : f.cycleFactorsFinset = { g } ↔ f.IsCycle ∧ f = g :=
  by
  suffices f = g → (g.IsCycle ↔ f.IsCycle) by
    rw [cycleFactorsFinset_eq_finset]
    simpa [eq_comm]
  rintro rfl
  exact Iff.rfl

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