powerSeriesFamily_of_orderTop_pos

Mathlib.RingTheory.HahnSeries.HEval

URI: https://scilib.ai/kg/mathlib#HahnSeries.SummableFamily.powerSeriesFamily_of_orderTop_pos

← MathLib Explorer

English

If a function's support is bounded below, then it is IsPWO (well-founded).

Русский

Если опора функции ограничена снизу, то она является IsPWO (хорошо упорядочено).

LaTeX

$$(Function.support f).IsPWO$$

Lean4

theorem powerSeriesFamily_of_orderTop_pos {x : HahnSeries Γ V} (hx : 0 < x.orderTop) (f : PowerSeries R) (n : ℕ) :
    powerSeriesFamily x f n = f.coeff n • x ^ n := by simp [hx]

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

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

Разделы

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

Аффилиация

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