isPWO_support

Mathlib.RingTheory.HahnSeries.Basic

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

English

The support of a Hahn series is partially well-ordered (IsPWO).

Русский

Поддержка ряда Хана частично хорошо упорядочена (IsPWO).

LaTeX

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

Lean4

@[simp]
theorem isPWO_support (x : HahnSeries Γ R) : x.support.IsPWO :=
  x.isPWO_support'

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

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

Разделы

Аффилиация

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