Commit 2024-12-11 04:11 43404d79

View on Github →

chore: used named arguments instead of @DecidableRel (#19850)

Estimated changes

modified theorem Finset.map_truncatedSup
modified theorem Finset.filter_infs_le
modified theorem Finset.filter_sups_le
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 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 theorem Interval.coe_iInf
modified theorem Interval.coe_iInf₂
modified theorem Interval.coe_sInf