compRel_swap

Mathlib.Order.Comparable

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

English

The relation CompRel is invariant under swapping the arguments of the underlying relation.

Русский

Отношение CompRel инвариантно при перестановке аргументов исходного отношения.

LaTeX

$$$\mathrm{CompRel}(\mathrm{swap}(r)) = \mathrm{CompRel}(r)$$$

Lean4

theorem compRel_swap (r : α → α → Prop) : CompRel (swap r) = CompRel r :=
  funext₂ fun _ _ ↦ propext or_comm

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

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

Разделы

Аффилиация

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