continuous_coeff

Mathlib.RingTheory.MvPowerSeries.PiTopology

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

← MathLib Explorer

English

For every d, the map coeff d from MvPowerSeries σ R to R is continuous.

Русский

Для каждого d отображение coeff d из MvPowerSeries σ R в R непрерывно.

LaTeX

$$Continuous(coeff(d))$$

Lean4

/-- `MvPowerSeries.coeff` is continuous. -/
@[fun_prop]
theorem continuous_coeff [Semiring R] (d : σ →₀ ℕ) : Continuous (MvPowerSeries.coeff (R := R) d) :=
  continuous_pi_iff.mp continuous_id d

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

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

Разделы

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

Аффилиация

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