ofIsMaxChain

Mathlib.Order.Preorder.Chain

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

English

A maximal chain c gives rise to a Flag α.

Русский

Максимальная цепь c порождает флаг α.

LaTeX

$$$\\\\forall c \\\\ hc, IsMaxChain (\\\\le) c \\\\rightarrow Flag α$$$

Lean4

/-- Reinterpret a maximal chain as a flag. -/
def ofIsMaxChain (c : Set α) (hc : IsMaxChain (· ≤ ·) c) : Flag α :=
  ⟨c, hc.isChain, hc.2⟩

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

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

Разделы

Аффилиация

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