Commit 2022-11-30 17:19 2f7863d7

View on Github →

chore: fix naming conventions in Order.WithBot (#801)

Estimated changes

added theorem WithBot.coe_strictMono
deleted theorem WithBot.coe_strict_mono
added theorem WithBot.recBotCoe_bot
added theorem WithBot.recBotCoe_coe
deleted theorem WithBot.rec_bot_coe_bot
deleted theorem WithBot.rec_bot_coe_coe
added theorem WithBot.strictMono_iff
deleted theorem WithBot.strict_mono_iff
added theorem WithBot.wellFounded_gt
added theorem WithBot.wellFounded_lt
deleted theorem WithBot.well_founded_gt
deleted theorem WithBot.well_founded_lt
added theorem WithTop.coe_strictMono
deleted theorem WithTop.coe_strict_mono
added theorem WithTop.recTopCoe_coe
added theorem WithTop.recTopCoe_top
deleted theorem WithTop.rec_top_coe_coe
deleted theorem WithTop.rec_top_coe_top
added theorem WithTop.strictMono_iff
deleted theorem WithTop.strict_mono_iff
added theorem WithTop.wellFounded_gt
added theorem WithTop.wellFounded_lt
deleted theorem WithTop.well_founded_gt
deleted theorem WithTop.well_founded_lt