suppBddBelow_supp_PWO

Mathlib.RingTheory.HahnSeries.Basic

URI: https://scilib.ai/kg/mathlib#HahnSeries.suppBddBelow_supp_PWO

English

If the support is bounded below, then it is well-founded in the order (IsPWO).

Русский

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

LaTeX

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

Lean4

theorem suppBddBelow_supp_PWO (f : Γ → R) (hf : BddBelow (Function.support f)) : (Function.support f).IsPWO :=
  hf.isWF.isPWO

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

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

Разделы

Аффилиация

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