instIsTopologicalGroupMulOpposite

English

If a group α is a topological group, then its opposite αᵐᵒᵖ is also a topological group.

Русский

Если группа α — топологическая группа, то её противоположная группа αᵐᵒᵖ тоже топологическая группа.

LaTeX

$$$IsTopologicalGroup(\alpha^{\mathrm{op}})$$$

Lean4

/-- If multiplication is continuous in `α`, then it also is in `αᵐᵒᵖ`. -/
@[to_additive /-- If addition is continuous in `α`, then it also is in `αᵃᵒᵖ`. -/
    ]
instance [Group α] [IsTopologicalGroup α] : IsTopologicalGroup αᵐᵒᵖ where

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