coe_toBoundedOrderHom — Mathlib

English

The coercion toBoundedOrderHom from a BoundLatticeHom equals the underlying coe.

Русский

Коэрсия к BoundedOrderHom от BoundLatticeHom равна базовому преобразованию.

LaTeX

$$$\\forall f:\\mathrm{BoundedLatticeHom}(\\alpha,\\beta),\\ \\mathrm{BoundedOrderHom.instFunLike.coe}(f.toBoundedOrderHom) = \\mathrm{BoundedLatticeHom.instFunLike.coe}(f)$$$

Lean4

@[simp]
theorem coe_toBoundedOrderHom (f : BoundedLatticeHom α β) : ⇑f.toBoundedOrderHom = f :=
  rfl

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