swap_le_mk

Mathlib.Order.Basic

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

English

The relation is preserved under swapping arguments: x.swap ≤ (b,a) iff x ≤ (a,b).

Русский

Отражение пары меняет координаты, не нарушая порядок: x.swap ≤ (b,a) эквивалентно x ≤ (a,b).

LaTeX

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

Lean4

@[simp]
theorem swap_le_mk : x.swap ≤ (b, a) ↔ x ≤ (a, b) :=
  and_comm

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

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

Разделы

Аффилиация

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