smul_set — Mathlib

English

If k and u are compact, then their product under the action is compact: k • u is compact.

Русский

Если k и u компактны, то их образ под действием также компактен: k • u компактно.

LaTeX

$$$IsCompact(k) \land IsCompact(u) \Rightarrow IsCompact(k \cdot u)$$$

Lean4

@[to_additive]
theorem smul_set {k : Set M} {u : Set X} (hk : IsCompact k) (hu : IsCompact u) : IsCompact (k • u) :=
  by
  rw [← Set.image_smul_prod]
  exact IsCompact.image (hk.prod hu) continuous_smul

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