instContinuousMulOrderDual — Mathlib

English

If M is a topological monoid, then its order dual M^op (with reversed multiplication) is also a topological monoid; the multiplication map is continuous in M^op.

Русский

Если M — топологическая моноида, то ее двойственный порядок M^op (с обращенной операцией умножения) также является топологической моноидой; умножение непрерывно в M^op.

LaTeX

$$$\text{ContinuousMul}(M^{\mathrm{op}})$$$

Lean4

@[to_additive]
instance : ContinuousMul Mᵒᵈ :=
  ‹ContinuousMul M›

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