le_or_le

Mathlib.Order.Preorder.Chain

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

English

Any two elements of a flag are comparable: a ≤ b or b ≤ a.

Русский

Любые два элемента флага сравнимы: либо a ≤ b, либо b ≤ a.

LaTeX

$$$\\\\forall a,b \\in s, a \\\\le b \\\\lor b \\\\le a$$$

Lean4

protected theorem le_or_le (s : Flag α) (ha : a ∈ s) (hb : b ∈ s) : a ≤ b ∨ b ≤ a :=
  s.chain_le.total ha hb

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

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

Разделы

Аффилиация

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