instProperConstSMulOfContinuousConstSMul

English

For every element g of a topological group G acting on a topological space X with a continuous constant smul, the map x ↦ g · x is a proper map.

Русский

Для каждого элемента g группы G, действующей на топологическом пространстве X, с непрерывным константным умножением, отображение x ↦ g · x является правильной (свойство proper).

LaTeX

$$$\\\\forall g \\\\in G, \\\\; f_g: X \\to X, \\; f_g(x) = g \\cdot x \\text{ is proper; i.e. } f_g^{-1}(K) \\\\text{ is compact for every compact } K \\subseteq X.$$$

Lean4

@[to_additive]
instance (priority := 100) {G X : Type*} [Group G] [MulAction G X] [TopologicalSpace X] [ContinuousConstSMul G X] :
    ProperConstSMul G X :=
  ⟨fun c ↦ (Homeomorph.smul c).isProperMap⟩

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