English
Extends a lattice homomorphism to the top-extended lattices by combining its Inf and Sup parts accordingly.
Русский
Расширяет гомоморфизм решёток до расширенных верхними элементами, объединяя части Inf и Sup.
LaTeX
$$$ \mathrm{withTop}(f) : \mathrm{LatticeHom}(\mathrm{WithTop}\ \alpha, \mathrm{WithTop}\ \beta) \\ \text{with toInfHom} = f^{\mathrm{Top}}.\mathrm{withTop}, \ \text{toSupHom} = f^{\mathrm{Top}}.\mathrm{withTop} $$$
Lean4
/-- Adjoins a `⊤` to the domain and codomain of a `LatticeHom`. -/
@[simps]
protected def withTop (f : LatticeHom α β) : LatticeHom (WithTop α) (WithTop β) :=
{ f.toInfHom.withTop with toSupHom := f.toSupHom.withTop }
-- Porting note: `simps` doesn't generate those
