quotient_finite_of_isOpen — Mathlib

English

If G is compact and U is an open subgroup, then the quotient G/U is finite.

Русский

Если G компактна и U — открытая подгруппа, то фактор-группа G/U конечна.

LaTeX

$$$$ |G/U| < \\infty. $$$$

Lean4

@[to_additive]
theorem quotient_finite_of_isOpen [ContinuousMul G] [CompactSpace G] (U : Subgroup G) (h : IsOpen (U : Set G)) :
    Finite (G ⧸ U) :=
  have : DiscreteTopology (G ⧸ U) := U.discreteTopology h
  finite_of_compact_of_discrete

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