mk_lt_swap

Mathlib.Order.Basic

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

English

Using swap_lt_swap, the mk version holds: (b,a) < x.swap iff (a,b) < x.

Русский

Используя swap_lt_swap, верно: (b,a) < x.swap эквивалентно (a,b) < x.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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