quotient_finite_of_isOpen' — Mathlib

English

Let G be a compact topological group with an open subgroup U, and K an open subgroup of U. Then the quotient U/K is finite (the index [U : K] is finite).

Русский

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

LaTeX

$$$|U : K| < \\infty$$$

Lean4

@[to_additive]
theorem quotient_finite_of_isOpen' [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) (K : Subgroup U)
    (hUopen : IsOpen (U : Set G)) (hKopen : IsOpen (K : Set U)) : Finite (U ⧸ K) :=
  have : CompactSpace U := isCompact_iff_compactSpace.mp <| IsClosed.isCompact <| U.isClosed_of_isOpen hUopen
  K.quotient_finite_of_isOpen hKopen

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