comp — Mathlib

English

The composition of two lattice homomorphisms is a lattice homomorphism.

Русский

Составление двух гомоморфизмов решетки образует гомоморфизм решетки.

LaTeX

$$$f:\mathrm{LatticeHom}(\beta,\gamma)$ and $g:\mathrm{LatticeHom}(\alpha,\beta)$ imply $f\circ g:\mathrm{LatticeHom}(\alpha,\gamma)$.$$

Lean4

/-- Composition of `LatticeHom`s as a `LatticeHom`. -/
def comp (f : LatticeHom β γ) (g : LatticeHom α β) : LatticeHom α γ :=
  { f.toSupHom.comp g.toSupHom, f.toInfHom.comp g.toInfHom with }

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