Commit 2025-09-25 05:18 80565ea4

View on Github →

chore: rely less on WithTop/Bot-Option defeq, add missing API (#29874) Nowhere near comprehensive; inspired by #27918.

Estimated changes

modified theorem ENNReal.coe_ofNNRealHom
modified theorem InfHom.withBot_id
modified theorem InfHom.withTop_id
modified theorem SupHom.withBot_id
modified theorem SupHom.withTop_id
added theorem WithBot.comp_map
added theorem WithBot.map_comp_map
added theorem WithBot.map_id
added theorem WithBot.map_map
added theorem WithTop.comp_map
added theorem WithTop.map_comp_map
added theorem WithTop.map_id
added theorem WithTop.map_map