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