instCompactSpaceSubtypeMem — Mathlib

English

If G is compact, then any ClosedSubgroup H yields a compact space for the subtype of elements belonging to H.

Русский

Если G компактна, то подгруппа H порождает компактное множество подпространства элементов H.

LaTeX

$$$ \\text{CompactSpace}(Subtype (\\lambda x, x \\in H)) $$$

Lean4

@[to_additive]
instance [CompactSpace G] (H : ClosedSubgroup G) : CompactSpace H :=
  isCompact_iff_compactSpace.mp (IsClosed.isCompact H.isClosed')

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