instProperConstSMulOfContinuousConstSMulOfT2SpaceOfCompactSpace

English

If M acts on X with a continuous constant smul and X is T2 and compact, then there is a properConstSMul instance.

Русский

Если M действует на X посредством непрерывного константного смула и X является T2 и компактным, то существует инстанс ProperConstSMul.

LaTeX

$$$\\exists$ ProperConstSMul M X under compact T2 assumptions$$

Lean4

@[to_additive]
instance (priority := 100) {M X : Type*} [SMul M X] [TopologicalSpace X] [ContinuousConstSMul M X] [T2Space X]
    [CompactSpace X] : ProperConstSMul M X :=
  ⟨fun c ↦ (continuous_const_smul c).isProperMap⟩

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