Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-10-05 07:59
245959d9
View on Github →
feat: {forall,exists}
ne
{top,bot} (
#30208
) Working towards
#27918
.
Estimated changes
Modified
Mathlib/Data/ENNReal/Basic.lean
modified
theorem
ENNReal.exists_ne_top
modified
theorem
ENNReal.forall_ne_top
Modified
Mathlib/Data/ENat/Basic.lean
added
theorem
ENat.exists_ne_top
added
theorem
ENat.forall_ne_top
Modified
Mathlib/Order/WithBot.lean
added
theorem
WithBot.exists_ne_bot
added
theorem
WithBot.forall_ne_bot
added
theorem
WithTop.exists_ne_top
added
theorem
WithTop.forall_ne_top
Modified
Mathlib/Topology/Instances/ENat.lean