compRel

Mathlib.Order.Comparable

URI: https://scilib.ai/kg/mathlib#AntisymmRel.compRel

English

Under IsTotal, every pair is comparable, hence CompRel r a b holds.

Русский

При IsTotal для любой пары элементов выполняется сравнимость, следовательно CompRel r a b.

LaTeX

$$$CompRel r a b$$$

Lean4

theorem compRel (h : AntisymmRel r a b) : CompRel r a b :=
  Or.inl h.1

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

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

Разделы

Аффилиация

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