isClosedMap_smul_of_ne_zero — Mathlib

English

Let c ≠ 0. The map x ↦ c • x on α is a closed map; i.e., it sends closed sets to closed sets.

Русский

Пусть c ≠ 0. Отображение x ↦ c • x на α является замкнутым отображением: образ замкнутого множества является замкнутым.

LaTeX

$$$IsClosedMap\ (x \mapsto c \cdot x)$$$

Lean4

/-- `smul` is a closed map in the second argument.

The lemma that `smul` is a closed map in the first argument (for a normed space over a complete
normed field) is `isClosedMap_smul_left` in `Analysis.Normed.Module.FiniteDimension`. -/
theorem isClosedMap_smul_of_ne_zero {c : G₀} (hc : c ≠ 0) : IsClosedMap fun x : α => c • x :=
  (Homeomorph.smulOfNeZero c hc).isClosedMap

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