English
Adjoins a top element to the codomain of a SupHom: the map is defined by toFun a := a.elim ⊤ f, and it preserves sup appropriately.
Русский
К верхнему элементу кодомного пространства SupHom добавляется верхний элемент: отображение задаётся как toFun a := a.elim ⊤ f и сохраняет операцию sup.
LaTeX
$$$ \text{toFun}(\mathrm{withTop}'(f))\,=\, (a \mapsto a\text{.elim } \top f) \,$$$
Lean4
/-- Adjoins a `⊤` to the codomain of a `SupHom`. -/
@[simps]
def withTop' [OrderTop β] (f : SupHom α β) : SupHom (WithTop α) β
where
toFun a := a.elim ⊤ f
map_sup' a
b :=
match a, b with
| ⊤, ⊤ => (top_sup_eq _).symm
| ⊤, (b : α) => (top_sup_eq _).symm
| (a : α), ⊤ => (sup_top_eq _).symm
| (a : α), (b : α) => f.map_sup' _ _
