continuousSMul — Mathlib

English

Let S be a Subalgebra R A. If X is a topological space with a MulAction by A and ContinuousSMul A X holds, then the restricted action by S on X is continuous.

Русский

Пусть S — подалгебра R A. Если X является топологическим пространством с действием умножения A на X и непрерывность действия A на X, то ограниченное действие S на X тоже непрерывно.

LaTeX

$$$\\operatorname{ContinuousSMul}~S~X$$$

Lean4

instance continuousSMul (S : Subalgebra R A) (X) [TopologicalSpace X] [MulAction A X] [ContinuousSMul A X] :
    ContinuousSMul S X :=
  Subsemiring.continuousSMul S.toSubsemiring X

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