Theorem WithTop.top_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.top_mem_insertTop View on Github →