swap_lt_mk

Mathlib.Order.Basic

URI: https://scilib.ai/kg/mathlib#Prod.swap_lt_mk

English

Simplicity of the comparison after swap: x.swap < (b,a) iff x < (a,b).

Русский

Упрощение сравнения после перестановки: x.swap < (b,a) эквивалентно x < (a,b).

LaTeX

$$$x.swap < (b,a) \iff x < (a,b)$$$

Lean4

@[simp]
theorem swap_lt_mk : x.swap < (b, a) ↔ x < (a, b) := by rw [← swap_lt_swap]; simp

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

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

Разделы

Аффилиация

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