cmpLE_swap — Mathlib

English

The swap of the comparison between x and y equals the comparison of y and x.

Русский

Замена порядка сравнения между x и y дает сравнение между y и x.

LaTeX

$$$\\forall x\\ y, (cmpLE x y).swap = cmpLE y x$$$

Lean4

theorem cmpLE_swap {α} [LE α] [IsTotal α (· ≤ ·)] [DecidableLE α] (x y : α) : (cmpLE x y).swap = cmpLE y x :=
  by
  by_cases xy : x ≤ y <;> by_cases yx : y ≤ x <;> simp [cmpLE, *, Ordering.swap]
  cases not_or_intro xy yx (total_of _ _ _)

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