disjoint_mul_inv_of_mem_cycleFactorsFinset

English

If f is a cycle factor of g, then the permutation g f^{-1} is disjoint from f.

Русский

Если f является фактором цикла g, то произведение g f^{-1} и f взаимно не имеют общих точек.

LaTeX

$$Disjoint (g * f^{-1}) f$$

Lean4

theorem disjoint_mul_inv_of_mem_cycleFactorsFinset {f g : Perm α} (h : f ∈ cycleFactorsFinset g) :
    Disjoint (g * f⁻¹) f := by
  rw [mem_cycleFactorsFinset_iff] at h
  intro x
  by_cases hx : f x = x
  · exact Or.inr hx
  · refine Or.inl ?_
    rw [mul_apply, ← h.right, apply_inv_self]
    rwa [← support_inv, apply_mem_support, support_inv, mem_support]

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