cmp_swap — Mathlib

English

Swapping the arguments of cmp reverses their order: (cmp a b).swap = cmp b a.

Русский

Обмен аргументов компаратора меняет их порядок: (cmp a b).swap = cmp b a.

LaTeX

$$$\\forall a\\ b,\\ (cmp a b).swap = cmp b a$$$

Lean4

@[simp]
theorem cmp_swap [Preorder α] [DecidableLT α] (a b : α) : (cmp a b).swap = cmp b a :=
  by
  unfold cmp cmpUsing
  by_cases h : a < b <;> by_cases h₂ : b < a <;> simp [h, h₂, Ordering.swap]
  exact lt_asymm h h₂

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