instTopologicalSpaceMulOpposite — Mathlib

English

The topology on the opposite monoid Mᵐᵒᵖ is defined as the induced topology by unop from M.

Русский

Топология на противоположном моноиде Mᵐᵒᵖ задаётся как индуцированная топология через отображение unop от M.

LaTeX

$$$$ \text{TopologicalSpace}(M^{\mathrm{op}}) = \mathrm{TopologicalSpace.induced}(\mathrm{unop}, \text{TopologicalSpace}(M)) $$$$

Lean4

/-- Put the same topological space structure on the opposite monoid as on the original space. -/
@[to_additive /-- Put the same topological space structure on the opposite monoid as on the original
    space. -/
    ]
instance instTopologicalSpaceMulOpposite [TopologicalSpace M] : TopologicalSpace Mᵐᵒᵖ :=
  TopologicalSpace.induced (unop : Mᵐᵒᵖ → M) ‹_›

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