chain_le

Mathlib.Order.Preorder.Chain

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

English

For any flag s, the relation ≤ defines a chain on its carrier.

Русский

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

LaTeX

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

Lean4

theorem chain_le (s : Flag α) : IsChain (· ≤ ·) (s : Set α) :=
  s.Chain'

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

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

Разделы

Аффилиация

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