finite_quotient_of_finite_quotient_of_index_ne_zero

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

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