English
Let α and β be preordered sets and f: α →o β an order-preserving map. Then there exists an order-preserving map F: WithTop α →o WithTop β extending f, obtained by F = WithTop.map f and with F(top) = top.
Русский
Пусть α и β — предмножества с упорядочиванием, и f: α →o β — отображение, сохраняющее порядок. Тогда существует отображение F: WithTop α →o WithTop β, сохраняющее порядок, такое что F ограничено есть f и F(top) = top, полученное как F = WithTop.map f.
LaTeX
$$$\\exists F:\\mathrm{WithTop}\\,\\alpha \\to_o \\mathrm{WithTop}\\,\\beta\\;\\big( F = \\mathrm{WithTop.map}\\, f \\;\\wedge\\; F(\\top)=\\top \\wedge\\; \\forall a:\\alpha,\\ F(a)=f(a) \\big)$.$$
Lean4
/-- Lift an order homomorphism `f : α →o β` to an order homomorphism `WithTop α →o WithTop β`. -/
@[simps -fullyApplied]
protected def withTopMap (f : α →o β) : WithTop α →o WithTop β :=
⟨WithTop.map f, f.mono.withTop_map⟩
