instFiniteQuotientOfContinuousMulOfCompactSpace

English

Let G be a compact topological group with continuous multiplication, and U an open subgroup of G. Then the quotient G/U has finitely many elements (i.e., the index [G : U] is finite).

Русский

Пусть G — компактная топологическая группа с непрерывным умножением, и U — открытая подгруппа G. Тогда фактор-группа G/U содержит конечное число элементов ( индекс [G : U] конечен ).

LaTeX

$$$|G : U| < \\infty$$$

Lean4

@[to_additive]
instance [ContinuousMul G] [CompactSpace G] (U : OpenSubgroup G) : Finite (G ⧸ U.toSubgroup) :=
  quotient_finite_of_isOpen U.toSubgroup U.isOpen

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