swap_le_swap

Mathlib.Order.Basic

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

English

Swapping the coordinates preserves the order: x.swap ≤ y.swap iff x ≤ y.

Русский

Перестановка координат сохраняет порядок: x.swap ≤ y.swap эквивалентно x ≤ y.

LaTeX

$$$x^{\text{swap}} \le y^{\text{swap}} \iff x \le y$$$

Lean4

@[simp]
theorem swap_le_swap : x.swap ≤ y.swap ↔ x ≤ y :=
  and_comm

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

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

Разделы

Аффилиация

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