finite_quotient_of_pretransitive_of_index_ne_zero

English

If H index ≠ 0 under a pretransitive G-action on X, then the quotient by H acting on X is finite.

Русский

При предтранзитивном действии G на X, если H.index ≠ 0, то квотиента по H на X конечна.

LaTeX

$$$[MulAction.G X] \land [MulAction.IsPretransitive G X] \land H.index \neq 0 \Rightarrow Finite(MulAction.orbitRel.Quotient H X)$$$

Lean4

@[to_additive]
theorem finite_quotient_of_pretransitive_of_index_ne_zero {X : Type*} [MulAction G X] [MulAction.IsPretransitive G X]
    (hi : H.index ≠ 0) : Finite <| MulAction.orbitRel.Quotient H X :=
  by
  have := (MulAction.pretransitive_iff_subsingleton_quotient G X).1 inferInstance
  exact finite_quotient_of_finite_quotient_of_index_ne_zero hi

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