instContinuousSMulSubtypeLeOfNat — Mathlib

English

Under the same hypotheses as the previous item, the induced action of the nonnegative scalars {r ∈ R | 0 ≤ r} on α is continuous.

Русский

При тех же предположениях, что и выше, полученное ограниченное действие неположительных скаляров на α непрерывно.

LaTeX

$$$\\forall R, \\alpha \\, [\\text{Semiring } R] [\\text{PartialOrder } R] [\\text{SMul } R \\alpha] [\\text{TopologicalSpace } \\alpha] [\\text{ContinuousConstSMul } R \\alpha], \\, \\text{ContinuousSMul} \\{ r : R \\mid 0 \\le r \\} \\alpha$$$

Lean4

instance [TopologicalSpace R] [ContinuousSMul R α] : ContinuousSMul { r : R // 0 ≤ r } α where
  continuous_smul := continuous_smul (M := R).comp <| continuous_subtype_val.prodMap continuous_id

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