withTop' — Mathlib

English

Adjoins a top to the codomain of a lattice homomorphism: a construction giving a lattice homomorphism from WithTop α to β.

Русский

Добавляет максимум к области значений отображения: конструирует гомоморфизм From WithTop α к β.

LaTeX

$$$ \\text{withTop'}(f) = \\{ f.\\mathrm{toSupHom}.\\mathrm{withTop'}, f.\\mathrm{toInfHom}.\\mathrm{withTop'} \\}$$$

Lean4

/-- Adjoins a `⊥` to the codomain of a `LatticeHom`. -/
@[simps]
def withTop' [OrderTop β] (f : LatticeHom α β) : LatticeHom (WithTop α) β :=
  { f.toSupHom.withTop', f.toInfHom.withTop' with }

Похожие утверждения