swap_eq_iff_eq_swap

Mathlib.Order.Compare

URI: https://scilib.ai/kg/mathlib#Ordering.swap_eq_iff_eq_swap

English

For any two orderings o and o', o.swap equals o' if and only if o equals o'.swap.

Русский

Для любых упорядочиваний o и o' выполняется: o.swap = o' тогда и только тогда, когда o = o'.swap.

LaTeX

$$$\\forall o\\ o',\n o.swap = o' \\leftrightarrow o = o'.swap$$$

Lean4

theorem swap_eq_iff_eq_swap {o o' : Ordering} : o.swap = o' ↔ o = o'.swap := by rw [← swap_inj, swap_swap]

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

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

Разделы

Аффилиация

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