preimage_smul — Mathlib

English

The preimage of a compact set under the map x ↦ c • x is compact when the action is a ProperConstSMul.

Русский

Обратное изображение компактного множества по отображению x ↦ c • x компактно, если действие является ProperConstSMul.

LaTeX

$$$\\text{IsCompact}( (c \\cdot \\cdot)^{-1}(s) )$ when $s$ is compact.$$

Lean4

/-- The preimage of a compact set under `(c • ·)` is a compact set. -/
@[to_additive /-- The preimage of a compact set under `(c +ᵥ ·)` is a compact set. -/
    ]
theorem preimage_smul {M X : Type*} [SMul M X] [TopologicalSpace X] [ProperConstSMul M X] {s : Set X} (hs : IsCompact s)
    (c : M) : IsCompact ((c • ·) ⁻¹' s) :=
  (isProperMap_smul c X).isCompact_preimage hs

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