English
Adjoins a top and bottom to the domain and codomain of a lattice homomorphism: from α → β to WithTop(WithBot α) → WithTop(WithBot β).
Русский
К отображению между решётками добавляются ⊤ и ⊥ к области определения и кодомапу: из α → β в WithTop(WithBot α) → WithTop(WithBot β).
LaTeX
$$$ \\mathrm{withTopWithBot}(f) : \\text{BoundedLatticeHom}(\\mathrm{WithTop}(\\mathrm{WithBot}\\, \\alpha), \\mathrm{WithTop}(\\mathrm{WithBot}\\, \\beta)) $$$
Lean4
/-- Adjoins a `⊤` and `⊥` to the domain and codomain of a `LatticeHom`. -/
@[simps]
def withTopWithBot (f : LatticeHom α β) : BoundedLatticeHom (WithTop <| WithBot α) (WithTop <| WithBot β) :=
⟨f.withBot.withTop, rfl, rfl⟩
-- Porting note: `simps` doesn't generate those
