English
A version of the construction that, given an order-embedding f: α ↪o β, yields an order-embedding from WithTop α to WithTop β defined by toFun := WithTop.map f and compatible with the dual/top structure. This provides an extension of f to the WithTop level that preserves order.
Русский
Версия построения, при наличии вложения порядка f: α ↪o β, даёт вложение From WithTop α к WithTop β, определённое как toFun := WithTop.map f и совместимое с верхней структурой. Такое расширение сохраняет порядок.
LaTeX
$$$\\exists F:\\mathrm{WithTop}\\,\\alpha \\hookrightarrowo \\mathrm{WithTop}\\,\\beta \\;\\big( F = \\mathrm{WithTop.map}\\, f \\big).$$$
Lean4
/-- A version of `WithTop.map` for order embeddings. -/
@[simps -fullyApplied]
protected def withTopMap (f : α ↪o β) : WithTop α ↪o WithTop β :=
{ f.dual.withBotMap.dual with toFun := WithTop.map f }
