argsRel_wf

Mathlib.SetTheory.Surreal.Multiplication

URI: https://scilib.ai/kg/mathlib#Surreal.Multiplication.argsRel_wf

English

The relation ArgsRel is well-founded.

Русский

Отношение ArgsRel является хорошо упорядоченным.

LaTeX

$$$$ \mathrm{WellFounded}(\mathrm{ArgsRel}). $$$$

Lean4

/-- `ArgsRel` is well-founded. -/
theorem argsRel_wf : WellFounded ArgsRel :=
  InvImage.wf _ wf_isOption.cutExpand.transGen

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

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

Разделы

Аффилиация

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