English
Adjoins a bottom element to both the domain and codomain of a LatticeHom, by extending Inf and Sup parts.
Русский
К нижнему элементу домена и кодомного пространства гомоморфизма решёток добавляется нижний элемент, путем расширения частей Inf и Sup.
LaTeX
$$$ \mathrm{withBot}(f) : \mathrm{LatticeHom}(\mathrm{WithBot}\ \alpha, \mathrm{WithBot}\ \beta) \\ = \{ \text{toInfHom} = f.{\mathrm{toInfHom}}.{\mathrm{withBot}}, \; \text{toSupHom} = f.{\mathrm{toSupHom}}.{\mathrm{withBot}} \} $$$
Lean4
/-- Adjoins a `⊥` to the domain and codomain of a `LatticeHom`. -/
@[simps]
protected def withBot (f : LatticeHom α β) : LatticeHom (WithBot α) (WithBot β) :=
{ f.toInfHom.withBot with toSupHom := f.toSupHom.withBot }
-- Porting note: `simps` doesn't generate those
