coe_to_lattice_hom — Mathlib

English

The coercion of toLatticeHom yields the same function as the original: the underlying function is preserved by the coercion.

Русский

Коэрценция toLatticeHom сохраняет исходную функцию при отображении в гомоморфизм решётки.

LaTeX

$$$\forall f, \bigl( \operatorname{toLatticeHom} (f)\bigr)(a) = f(a) \text{ for all } a. $$$

Lean4

@[simp]
theorem coe_to_lattice_hom (f : F) : ⇑(toLatticeHom α β f) = f :=
  rfl

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