toBoundedOrderHom — Mathlib

English

There is a canonical reinterpretation from BoundLatticeHom to BoundedOrderHom.

Русский

Существует каноническое преобразование из BoundLatticeHom к BoundedOrderHom.

LaTeX

$$$\\text{toBoundedOrderHom}(f):=\\text{BoundedOrderHom}(\\alpha,\\beta)$ for $f:\\mathrm{BoundedLatticeHom}(\\alpha,\\beta)$$$

Lean4

/-- Reinterpret a `BoundedLatticeHom` as a `BoundedOrderHom`. -/
def toBoundedOrderHom (f : BoundedLatticeHom α β) : BoundedOrderHom α β :=
  { f, (f.toLatticeHom : α →o β) with }

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