decidableRel

Mathlib.Order.Comparable

URI: https://scilib.ai/kg/mathlib#CompRel.decidableRel

English

If AntisymmRel r a b holds, then CompRel r a b holds.

Русский

Если AntisymmRel r a b выполняется, тогда CompRel r a b выполняется.

LaTeX

$$$AntisymmRel r a b \Rightarrow CompRel r a b$$$

Lean4

instance decidableRel [DecidableRel r] : DecidableRel (CompRel r) := fun _ _ ↦ inferInstanceAs (Decidable (_ ∨ _))

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

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

Разделы

Аффилиация

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