mulLeft_continuous — Mathlib

English

In a topological semiring, the left-multiplication AddMonoidHom is continuous.

Русский

В топологическом полукольце лево-умножение является непрерывным отображением.

LaTeX

$$mulLeft_continuous (x)$$

Lean4

/-- In a topological semiring, the left-multiplication `AddMonoidHom` is continuous. -/
theorem mulLeft_continuous (x : R) : Continuous (AddMonoidHom.mulLeft x) :=
  continuous_const.mul continuous_id

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