Theorem BotHom.coe_inf

Modification history

2026-03-08 15:07

Mathlib/Order/Hom/Bounded.lean

chore(Order/Hom/Bounded): use `to_dual` (#36354)

Deleted BotHom.coe_inf View on Github →

2023-01-17 09:34

Mathlib/Order/Hom/Bounded.lean

feat: port Order.Hom.Bounded (#888) …

Added BotHom.coe_inf View on Github →