coe_toInfTopHom — Mathlib

English

The coercion to InfTopHom from a BoundLatticeHom agrees with the underlying coe.

Русский

Коэрсия к InfTopHom от BoundLatticeHom совпадает с базовым преобразованием.

LaTeX

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

Lean4

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

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