isWF_support

Mathlib.RingTheory.HahnSeries.Basic

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

English

The support of a Hahn series is well-founded (IsWF).

Русский

Опора ряда Хана хорошо основана (IsWF).

LaTeX

$$$\\text{(support(x)).IsWF}$$$

Lean4

@[simp]
theorem isWF_support (x : HahnSeries Γ R) : x.support.IsWF :=
  x.isPWO_support.isWF

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

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

Разделы

Аффилиация

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