smul — Mathlib

English

If s ⊆ β is compact and a ∈ α acts on β by a • x, then a • s is compact in α.

Русский

Если s ⊆ β компактно и есть действие a • x на β, то образ a • s компактен в β.

LaTeX

$$$ \\operatorname{IsCompact}(s) \\Rightarrow \\operatorname{IsCompact}(a \\cdot s) $$$

Lean4

@[to_additive]
theorem smul {α β} [SMul α β] [TopologicalSpace β] [ContinuousConstSMul α β] (a : α) {s : Set β} (hs : IsCompact s) :
    IsCompact (a • s) :=
  hs.image (continuous_id.const_smul a)

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