continuousSMul — Mathlib

English

Let M act continuously on a topological space X. Then the induced action of M on the opposite space Xᵐᵒᵖ is also continuous.

Русский

Пусть M действует непрерывно на топологическом пространстве X. Тогда индуцированное действие M на противоположном пространстве Xᵐᵒᵖ также непрерывно.

LaTeX

$$$ContinuousSMul\ M\ X^{\mathrm{op}}$$$

Lean4

@[to_additive]
instance continuousSMul : ContinuousSMul M Xᵐᵒᵖ :=
  ⟨MulOpposite.continuous_op.comp <| continuous_smul.comp <| continuous_id.prodMap MulOpposite.continuous_unop⟩

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