Commit 2025-10-05 07:59 245959d9

View on Github →

feat: {forall,exists}ne{top,bot} (#30208) Working towards #27918.

Estimated changes

modified theorem ENNReal.exists_ne_top
modified theorem ENNReal.forall_ne_top
added theorem ENat.exists_ne_top
added theorem ENat.forall_ne_top
added theorem WithBot.exists_ne_bot
added theorem WithBot.forall_ne_bot
added theorem WithTop.exists_ne_top
added theorem WithTop.forall_ne_top