English
Adjoins a bottom element to the domain of a SupHom: the map is defined by toFun a := a.elim ⊥ f, and it preserves sup accordingly.
Русский
Книзу добавляется нижний элемент домена для SupHom: отображение задаётся как toFun a := a.elim ⊥ f, и сохраняет sup.
LaTeX
$$$ \text{toFun}(\mathrm{withBot}'(f))\,=\, (a \mapsto a\text{.elim } \bot f) \,$$$
Lean4
/-- Adjoins a `⊥` to the domain of a `SupHom`. -/
@[simps]
def withBot' [OrderBot β] (f : SupHom α β) : SupBotHom (WithBot α) β
where
toFun a := a.elim ⊥ f
map_sup' a
b :=
match a, b with
| ⊥, ⊥ => (bot_sup_eq _).symm
| ⊥, (b : α) => (bot_sup_eq _).symm
| (a : α), ⊥ => (sup_bot_eq _).symm
| (a : α), (b : α) => f.map_sup' _ _
map_bot' := rfl
