maxChain

Mathlib.Order.Preorder.Chain

URI: https://scilib.ai/kg/mathlib#Flag.maxChain

English

Every flag has a maximal chain under the order.

Русский

Каждый флаг имеет максимальную цепь относительно порядка.

LaTeX

$$$\\\\forall s : Flag α, IsMaxChain (\\\\le) (s : Set α)$$$

Lean4

protected theorem maxChain (s : Flag α) : IsMaxChain (· ≤ ·) (s : Set α) :=
  ⟨s.chain_le, s.max_chain'⟩

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

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

Разделы

Аффилиация

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