Theorem WithBot.coe_biInf

Modification history

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