Theorem WithBot.coe_biSup

Modification history

2025-11-29 05:38
Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
feat(Order): coercion to `WithBot α` commutes with `biSup` (#26287) …
Added WithBot.coe_biSupView on Github →