toInfHom — Mathlib

English

Every lattice homomorphism can be regarded as an infimum-preserving map; there is a canonical inclusion that identifies LatticeHom(α,β) with a subset of InfHom(α,β).

Русский

Каждый гомоморфизм решетки можно рассматривать как сохраняющий пересечение; существует каноническое вложение, идентифицирующее LatticeHom(α,β) в InfHom(α,β).

LaTeX

$$$\text{There is a natural map }\iota: \mathrm{LatticeHom}(\alpha,\beta) \to \mathrm{InfHom}(\alpha,\beta) \text{ defined by } \iota(f) = f \text{ (as an InfHom).}$$$

Lean4

/-- Reinterpret a `LatticeHom` as an `InfHom`. -/
def toInfHom (f : LatticeHom α β) : InfHom α β :=
  { f with }

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