Commit 2025-12-28 23:05 23ce1f3f

View on Github →

chore(Order/WithBot): use to_dual (part 4) (#33267)

Estimated changes

modified theorem WithBot.le_ofDual_iff
modified theorem WithBot.le_toDual_iff
modified theorem WithBot.lt_ofDual_iff
modified theorem WithBot.lt_toDual_iff
modified theorem WithBot.map_ofDual
modified theorem WithBot.map_toDual
modified theorem WithBot.ofDual_apply_bot
modified theorem WithBot.ofDual_apply_coe
modified theorem WithBot.ofDual_le_iff
modified theorem WithBot.ofDual_lt_iff
modified theorem WithBot.ofDual_map
modified theorem WithBot.ofDual_symm_apply
modified theorem WithBot.toDual_apply_bot
modified theorem WithBot.toDual_apply_coe
modified theorem WithBot.toDual_le_iff
modified theorem WithBot.toDual_lt_iff
modified theorem WithBot.toDual_map
modified theorem WithBot.toDual_symm_apply
modified theorem WithTop.coe_mono
modified theorem WithTop.coe_strictMono
deleted theorem WithTop.le_ofDual_iff
deleted theorem WithTop.le_toDual_iff
deleted theorem WithTop.lt_ofDual_iff
deleted theorem WithTop.lt_toDual_iff
deleted theorem WithTop.map_ofDual
deleted theorem WithTop.map_toDual
modified theorem WithTop.monotone_iff
modified theorem WithTop.monotone_map_iff
deleted theorem WithTop.ofDual_apply_coe
deleted theorem WithTop.ofDual_apply_top
deleted theorem WithTop.ofDual_le_iff
deleted theorem WithTop.ofDual_lt_iff
deleted theorem WithTop.ofDual_map
deleted theorem WithTop.ofDual_symm_apply
modified theorem WithTop.strictAnti_iff
modified theorem WithTop.strictMono_iff
modified theorem WithTop.strictMono_map_iff
deleted theorem WithTop.toDual_apply_coe
deleted theorem WithTop.toDual_apply_top
deleted theorem WithTop.toDual_le_iff
deleted theorem WithTop.toDual_lt_iff
deleted theorem WithTop.toDual_map
deleted theorem WithTop.toDual_symm_apply