continuousSMul_of_algebraMap — Mathlib

English

Let R be a topological commutative semiring and A a topological R-algebra. If the map algebraMap: R → A is continuous and multiplication on A is continuous, then the scalar action R × A → A is continuous.

Русский

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

LaTeX

$$$\\operatorname{ContinuousSMul}~R~A$$$

Lean4

theorem continuousSMul_of_algebraMap [ContinuousMul A] (h : Continuous (algebraMap R A)) : ContinuousSMul R A :=
  ⟨(continuous_algebraMap_iff_smul R A).1 h⟩

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