Theorem WithBot.bot_covBy_coe

Modification history

2026-04-21 17:27

Mathlib/Order/Cover.lean

chore(Order/Interval/Set/WithBotTop): use `to_dual` (#38240)

Deleted WithBot.bot_covBy_coe View on Github →

2024-08-23 15:37

Mathlib/Order/Cover.lean

feat(Order/Cover): add lemmas about `WithTop`/`WithBot` (#15487)

Added WithBot.bot_covBy_coe View on Github →