English
If G acts on a set X and the quotient by G is finite, then the quotient by H is finite whenever H ≤ G and H.index ≠ 0 (under suitable hypotheses about the action).
Русский
Пусть G действует на множество X, и квотиента по G конечна; тогда когда H ≤ G и index(H) ≠ 0, квотиента по H конечна (при подходящих условиях действия).
LaTeX
$$$[\text{MulAction }G X] \land [Finite(\text{MulAction.orbitRel. Quotient } G X)] \land H.index \neq 0 \Rightarrow Finite(\text{MulAction.orbitRel.Quotient } H X)$$$
Lean4
@[to_additive]
theorem finite_quotient_of_finite_quotient_of_index_ne_zero {X : Type*} [MulAction G X]
[Finite <| MulAction.orbitRel.Quotient G X] (hi : H.index ≠ 0) : Finite <| MulAction.orbitRel.Quotient H X :=
by
have := fintypeOfIndexNeZero hi
exact MulAction.finite_quotient_of_finite_quotient_of_finite_quotient