English
Let α and β be preordered sets and f: α ↪o β an order-embedding. Then there exists an order-embedding F: WithBot α ↪o WithBot β extending f, defined by F.toFun = WithBot.map f, F.inj' = WithBot.map_injective f.injective, and F.map_rel_iff' = WithBot.map_le_iff f f.map_rel_iff.
Русский
Пусть α и β — предмножества с упорядочиванием, и f: α ↪o β — вложение сохраняющее порядок. Тогда существует вложение F: WithBot α ↪o WithBot β, такое что F.toFun = WithBot.map f, F.inj' = Injetive, и F.map_rel_iff' задаются аналогично.
LaTeX
$$$\\exists F:\\mathrm{WithBot}\\,\\alpha \\hookrightarrowo \\mathrm{WithBot}\\,\\beta\\;\\big( F.toFun = \\mathrm{WithBot.map}\\, f \\wedge\\; F.inj' = \\mathrm{map\\_inj} \\wedge\\; F.map\\_rel\\_iff' = \\mathrm{map\\_rel\\_iff} \\big).$$$
Lean4
/-- A version of `WithBot.map` for order embeddings. -/
@[simps -fullyApplied]
protected def withBotMap (f : α ↪o β) : WithBot α ↪o WithBot β
where
toFun := WithBot.map f
inj' := WithBot.map_injective f.injective
map_rel_iff' := WithBot.map_le_iff f f.map_rel_iff
