coe_toLatticeHom — Mathlib

English

The coercion from toLatticeHom is equal to the underlying coe of the BoundLatticeHom.

Русский

Приведение к toLatticeHom эквивалентно встроенной коэрсионной функции BoundLatticeHom.

LaTeX

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

Lean4

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

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