swap_le_swap_iff — Mathlib

English

Swapping the two components of the sum preserves the order: a.swap ≤ b.swap if and only if a ≤ b.

Русский

Перестановка двух компонент суммы сохраняет порядок: a.swap ≤ b.swap тогда же, что и a ≤ b.

LaTeX

$$$a.swap \le b.swap \iff a \le b$ for all $a,b \in \alpha \oplus \beta$.$$

Lean4

@[simp]
theorem swap_le_swap_iff [LE α] [LE β] {a b : α ⊕ β} : a.swap ≤ b.swap ↔ a ≤ b :=
  liftRel_swap_iff

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