incompRel_swap_apply

Mathlib.Order.Comparable

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

English

For all a,b in α and relation r, IncompRel (swap r) a b is equivalent to IncompRel r a b.

Русский

Для любых a,b∈α и r: IncompRel(перестановка r) a b эквивалентно IncompRel r a b.

LaTeX

$$$IncompRel(\mathrm{swap}(r)) a b \leftrightarrow IncompRel(r) a b$$$

Lean4

theorem incompRel_swap_apply : IncompRel (swap r) a b ↔ IncompRel r a b :=
  antisymmRel_swap_apply rᶜ

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

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

Разделы

Аффилиация

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