cmp_eq_cmp_symm — Mathlib

English

If cmp x y = cmp x' y' then cmp y x = cmp y' x'. In words, equality of compares is preserved by swapping arguments.

Русский

Если cmp x y = cmp x' y', то cmp y x = cmp y' x' (симметрия по перестановке аргументов).

LaTeX

$$$\mathrm{cmp}(x,y) = \mathrm{cmp}(x',y') \Rightarrow \mathrm{cmp}(y,x) = \mathrm{cmp}(y',x')$$$

Lean4

theorem cmp_eq_cmp_symm : cmp x y = cmp x' y' ↔ cmp y x = cmp y' x' :=
  ⟨fun h => by rwa [← cmp_swap x', ← cmp_swap, swap_inj], fun h => by rwa [← cmp_swap y', ← cmp_swap, swap_inj]⟩

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