Commit 2026-01-24 13:47 384649e3

View on Github →

feat(WithTop): add WithTop.add_lt_add and reuse in ENNReal (#34016)

  • resolve TODO: add WithTop.add_lt_add and use it for ENNReal.add_lt_add
  • resolve TODO: replace addLECancellable_iff_ne proof with WithTop.addLECancellable_iff_ne_top

Estimated changes