isProperMap_smul — Mathlib

English

For any M and X with a ProperConstSMul, the map x ↦ c • x is a proper map for any c ∈ M.

Русский

Для любых M и X с ProperConstSMul, отображение x ↦ c • x является правильным отображением для любого c ∈ M.

LaTeX

$$$\\text{IsProperMap} (\\lambda x, c \\cdot x)$$$

Lean4

/-- `(c • ·)` is a proper map. -/
@[to_additive /-- `(c +ᵥ ·)` is a proper map. -/
    ]
theorem isProperMap_smul {M : Type*} (c : M) (X : Type*) [SMul M X] [TopologicalSpace X] [h : ProperConstSMul M X] :
    IsProperMap ((c • ·) : X → X) :=
  h.1 c

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