Theorem WithBot.sInf_empty

Modification history

2026-06-02 12:39
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
feat(Order/ConditionallyCompleteLattice/Basic): more `WithTop` instances (#38890) …
Deleted WithBot.sInf_emptyView on Github →
2025-11-29 05:38
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
feat(Order): coercion to `WithBot α` commutes with `biSup` (#26287) …
Added WithBot.sInf_emptyView on Github →