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