Commit 2025-03-06 02:45 c99eb62b

View on Github →

feat(Order/Comparable): comparability/incomparability relations (#19580) We define two new relations for comparability and incomparability in a preorder, and introduce basic API for them. See this comment for an explanation of why we want both. This will be used in the new CGT repo to define the fuzzy relation x ‖ y = IncompRel (· ≤ ·) x y.

Estimated changes

modified theorem AntisymmRel.ge
modified theorem AntisymmRel.le
added theorem antisymmRel_swap_apply
added theorem AntisymmRel.compRel
added theorem CompRel.of_ge
added theorem CompRel.of_gt
added theorem CompRel.of_le
added theorem CompRel.of_lt
added theorem CompRel.of_rel
added theorem CompRel.of_rel_symm
added theorem CompRel.refl
added theorem CompRel.rfl
added theorem CompRel.symm
added def CompRel
added theorem IncompRel.not_ge
added theorem IncompRel.not_gt
added theorem IncompRel.not_le
added theorem IncompRel.not_lt
added theorem IncompRel.refl
added theorem IncompRel.rfl
added theorem IncompRel.symm
added def IncompRel
added theorem IsTotal.compRel
added theorem IsTotal.not_incompRel
added theorem LE.le.not_incompRel
added theorem LT.lt.not_incompRel
added theorem antisymmRel_compl
added theorem compRel_comm
added theorem compRel_swap
added theorem compRel_swap_apply
added theorem incompRel_comm
added theorem incompRel_compl
added theorem incompRel_compl_apply
added theorem incompRel_swap
added theorem incompRel_swap_apply
added theorem not_compRel_iff
added theorem not_incompRel_iff