trichotomous_of

Mathlib.Order.Defs.Unbundled

URI: https://scilib.ai/kg/mathlib#trichotomous_of

English

If r is trichotomous, then for any a,b, a ≺ b ∨ a = b ∨ b ≺ a.

Русский

Если r тричотомично, то для любых a,b: a ≺ b ∨ a = b ∨ b ≺ a.

LaTeX

$$$\forall a,b:\alpha, a \prec b \lor a = b \lor b \prec a$$$

Lean4

@[elab_without_expected_type]
theorem trichotomous_of [IsTrichotomous α r] : ∀ a b : α, a ≺ b ∨ a = b ∨ b ≺ a :=
  trichotomous

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

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

Разделы

Аффилиация

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