of_finite_mulAction_orbitRel_quotient

English

If G and Ω are finite, then α is finite.

Русский

Если G и Ω конечны, то α конечно.

LaTeX

$$Finite α$$

Lean4

@[to_additive]
theorem _root_.Finite.of_finite_mulAction_orbitRel_quotient [Finite G] [Finite Ω] : Finite α :=
  by
  rw [(selfEquivSigmaOrbits' G _).finite_iff]
  have : ∀ g : Ω, Finite g.orbit := by
    intro g
    induction g using Quotient.inductionOn'
    simpa [Set.finite_coe_iff] using Finite.finite_mulAction_orbit _
  exact Finite.instSigma

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