Commit 2025-03-05 05:17 bcf936b5

View on Github →

feat: WithBot.insertBot (#22523) This PR adds WithBot.insertBot, which was not added in #22477.

Estimated changes

Modified Mathlib/Order/Hom/Basic.lean

added def Function.Embedding.coeWithBot

Modified Mathlib/Order/Interval/Finset/Defs.lean

added theorem WithBot.bot_mem_insertBot

added def WithBot.insertBot

added theorem WithBot.some_mem_insertBot