Commit 2025-03-17 06:31 c5585bda

View on Github →

chore: Migrate to DecidableLT and DecidableLE (#22238) This PR changes DecidableRel (· ≤ ·) to DecidableLE and DecidableRel (· < ·) to DecidableLT.

Estimated changes

modified theorem Finset.map_truncatedSup
modified theorem Finset.filter_infs_le
modified theorem Finset.filter_sups_le
modified def cmp
modified def Ordnode.image
modified theorem Ordnode.Valid'.erase_aux
modified theorem Ordnode.dual_insert
modified theorem Ordnode.erase.valid
modified theorem Ordnode.insert'.valid
modified theorem Ordnode.insert.valid
modified theorem Ordnode.insertWith.valid
modified theorem Ordnode.pos_size_of_mem
modified theorem Ordnode.size_erase_of_mem
modified def Ordset.erase
modified theorem StrictMono.sign_comp
modified theorem sign_intCast
modified def cmpLE
modified theorem cmpLE_eq_cmp
modified theorem cmpLE_ofDual
modified theorem cmpLE_swap
modified theorem cmpLE_toDual
modified theorem cmp_ofDual
modified theorem cmp_swap
modified theorem cmp_toDual
modified def maxDefault
modified def minDefault
modified def Estimator.fstInst
modified theorem Interval.coe_iInf
modified theorem Interval.coe_iInf₂
modified theorem Interval.coe_sInf
modified theorem inf_eq_minDefault
modified theorem sup_eq_maxDefault