isCompact_compactSet — Mathlib

English

The fundamental cone compactSet is preserved under expansion by expMapBasis.

Русский

Фундаментальная конусная компактная область сохраняется под расширением expMapBasis.

LaTeX

$$expMapBasis '' Set.univ.pi ... ⊆ compactSet K$$

Lean4

theorem isCompact_compactSet : IsCompact (compactSet K) :=
  by
  refine
    isCompact_Icc.smul_set <|
      (isCompact_univ_pi fun w ↦ ?_).image_of_continuousOn (continuous_expMapBasis K).continuousOn
  split_ifs
  · exact isCompact_singleton
  · exact isCompact_Icc

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