finite_quotient_of_finite_quotient_of_finite_quotient

English

If the action is free and transitive, orbits of H on β correspond to cosets in α/H; a canonical equivalence β/H ≃ α/H.

Русский

При свободном и транзитивном действии орбиты H на β соответствуют косетам в α/H; существует каноническое эквивалентство β/H ≃ α/H.

LaTeX

$$orbitRel.Quotient (Subtype fun x => ...) β ≃ HasQuotient.Quotient α H$$

Lean4

@[to_additive]
instance finite_quotient_of_finite_quotient_of_finite_quotient {H : Subgroup α} [Finite (orbitRel.Quotient α β)]
    [Finite (α ⧸ H)] : Finite <| orbitRel.Quotient H β :=
  by
  rw [(equivSubgroupOrbits β H).finite_iff]
  infer_instance

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