instProperConstSMulProd — Mathlib

English

If a group M acts on topological spaces X and Y with continuous constant smul, then the induced action on X × Y is proper for each fixed group element.

Русский

Если группа M действует на топологических пространствах X и Y константным умножением непрерывно, то действие на произведение X × Y по каждому фиксированному элементу группы является правильным.

LaTeX

$$$\\forall c \\in M,\\; f_c^{X\\times Y}: X \\times Y \\to X \\times Y,\\; (x,y) \\mapsto (c\\cdot x, c\\cdot y)\\text{ is proper.}$$$

Lean4

instance {M X Y : Type*} [SMul M X] [TopologicalSpace X] [ProperConstSMul M X] [SMul M Y] [TopologicalSpace Y]
    [ProperConstSMul M Y] : ProperConstSMul M (X × Y) :=
  ⟨fun c ↦ (isProperMap_smul c X).prodMap (isProperMap_smul c Y)⟩

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