Def WithTop.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.insertTop View on Github →