continuousConstSMul' — Mathlib

English

If a topological space α carries a continuous constant action of a monoid M, then α also carries the corresponding continuous constant action of the order-dual monoid Mᵒᵈ with the same topology.

Русский

Пусть топологическое множество α имеет непрерывное константное действие моноида M; тогда для противоположного порядка моноида Mᵒᵈ на α сохраняется такое же непрерывное константное действие.

LaTeX

$$$ \\mathrm{ContinuousConstSMul}(M, \\alpha) \\Rightarrow \\mathrm{ContinuousConstSMul}(M^{\\mathrm{op}}, \\alpha) $$$

Lean4

@[to_additive]
instance continuousConstSMul' : ContinuousConstSMul Mᵒᵈ α :=
  ‹ContinuousConstSMul M α›

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