instContinuousMul — Mathlib

English

If multiplication is continuous in A, then multiplication on A^op is also continuous.

Русский

Если умножение непрерывно в A, то умножение в A^op также непрерывно.

LaTeX

$$$\\text{ContinuousMul } A \\Rightarrow \\text{ContinuousMul } A^{\\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 [TopologicalSpace α] [Mul α] [ContinuousMul α] : ContinuousMul αᵐᵒᵖ :=
  ⟨continuous_op.comp (continuous_unop.snd'.mul continuous_unop.fst')⟩

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