Mathlib Changelog
v4
Changelog
About
Github
Theorem
WithTop.some_mem_insertTop
Modification history
2025-03-03 09:04
Mathlib/Order/Interval/Finset/Defs.lean
chore: stop conflating WithTop and Option in WithTop.locallyFiniteOrder (#22477)
Added
WithTop.some_mem_insertTop
View on Github →