chainHeight_eq_iSup_subtype

Mathlib.Order.Height

URI: https://scilib.ai/kg/mathlib#Set.chainHeight_eq_iSup_subtype

English

The chain height equals the iSup of the cast lengths of subchains.

Русский

Высота цепи равна супремуму длин подцепей, приведённых к ENat.

LaTeX

$$$ s.\\mathrm{chainHeight} = \\bigvee_{l \\in s.\\mathrm{subchain}} (l.1.length)^↑. $$$

Lean4

theorem chainHeight_eq_iSup_subtype : s.chainHeight = ⨆ l : s.subchain, ↑l.1.length :=
  iSup_subtype'

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

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

Разделы

Аффилиация

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