chain_lt

Mathlib.Order.Preorder.Chain

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

English

For any flag s, the set s is chain under the strict order <.

Русский

Для любого флага s множество s образует цепь относительно строгого отношения <.

LaTeX

$$$\\\\forall s : Flag α, IsChain (\\\\lt) (s : Set α)$$$

Lean4

theorem chain_lt (s : Flag α) : IsChain (· < ·) (s : Set α) :=
  s.chain_le.lt_of_le

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

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

Разделы

Аффилиация

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