continuous_C — Mathlib

English

Let R be a topological semiring. The map sending each r ∈ R to the constant power series with value r is continuous.

Русский

Пусть R — топологический полугрупп. Отображение r → константный степенной ряд с коэффициентом r непрерывно.

LaTeX

$$$\mathrm{Continuous}(C)$$$

Lean4

theorem continuous_C [Semiring R] : Continuous (C (R := R)) :=
  MvPowerSeries.WithPiTopology.continuous_C

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