le_total

Mathlib.Algebra.Order.CauSeq.Basic

URI: https://scilib.ai/kg/mathlib#CauSeq.le_total

English

For any f,g, either f ≤ g or g ≤ f.

Русский

Для любых f,g либо f ≤ g или g ≤ f.

LaTeX

$$$\forall f,g \in \mathrm{CauSeq}(\alpha, \mathrm{abs}),\; f \le g \lor g \le f.$$$

Lean4

theorem le_total (f g : CauSeq α abs) : f ≤ g ∨ g ≤ f :=
  (or_assoc.2 (lt_total f g)).imp_right Or.inl

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

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

Разделы

Аффилиация

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