continuousSMul — Mathlib

English

If X is a space with a continuous action of R on X and S is a subring of R, then the restricted action of S on X is continuous.

Русский

Если X имеет непрерывное действие R на X, и S ⊆ R — подкольцо, то ограниченное действие S на X непрерывно.

LaTeX

$$ContinuousSMul S X$$

Lean4

instance continuousSMul (s : Subring R) (X) [TopologicalSpace X] [MulAction R X] [ContinuousSMul R X] :
    ContinuousSMul s X :=
  Subsemiring.continuousSMul s.toSubsemiring X

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