instContinuousSMulOfReal — Mathlib

English

If α is a topological space with a continuous real action, then restricting to NNReal gives a continuous action on α.

Русский

Если пространство α имеет непрерывное действие действительных чисел, то ограничение на неотрицательные числа даёт непрерывное действие на α.

LaTeX

$$$ \text{ContinuousSMul } \mathbb{R}_{\ge 0} \alpha $.$$

Lean4

instance [TopologicalSpace α] [MulAction ℝ α] [ContinuousSMul ℝ α] : ContinuousSMul ℝ≥0 α where
  continuous_smul := continuous_induced_dom.fst'.smul continuous_snd

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