swap_lt_swap — Mathlib

English

With Preorder on α and β, swapping coordinates preserves the lt relation: x.swap < y.swap iff x < y.

Русский

При наличии предпорядка на α и β, обмен координат сохраняет отношение строгого порядка: x.swap < y.swap эквивалентно x < y.

LaTeX

$$$x.swap < y.swap \iff x < y$$$

Lean4

@[simp]
theorem swap_lt_swap : x.swap < y.swap ↔ x < y :=
  and_congr swap_le_swap (not_congr swap_le_swap)

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