English
If G is a topological group that is compact, and U is an open subgroup of G with K an open subgroup of U, then the quotient U/K is finite.
Русский
Если G — компактная топологическая группа, U — открытая подгруппа G, и K — открытая подгруппа внутри U, то U/K конечна.
LaTeX
$$$|U : K| < \\infty$$$
Lean4
@[to_additive]
instance [IsTopologicalGroup G] [CompactSpace G] (U : OpenSubgroup G) (K : OpenSubgroup U) :
Finite (U ⧸ K.toSubgroup) :=
quotient_finite_of_isOpen' U.toSubgroup K.toSubgroup U.isOpen K.isOpen
