continuous_constantCoeff

Mathlib.RingTheory.MvPowerSeries.PiTopology

URI: https://scilib.ai/kg/mathlib#MvPowerSeries.WithPiTopology.continuous_constantCoeff

← MathLib Explorer

English

The map constantCoeff is continuous.

Русский

Отображение constantCoeff непрерывно.

LaTeX

$$Continuous(constantCoeff (\sigma := σ) (R := R))$$

Lean4

/-- `MvPowerSeries.constantCoeff` is continuous -/
theorem continuous_constantCoeff [Semiring R] : Continuous (constantCoeff (σ := σ) (R := R)) :=
  continuous_coeff (R := R) 0

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru