comp — Mathlib

English

The composition of two bounded lattice homomorphisms is again a bounded lattice homomorphism.

Русский

Сжатие двух гомоморфизмов ограниченной решетки образует новый гомоморфизм.

LaTeX

$$$\\forall f:\\mathrm{BoundedLatticeHom}(\\beta,\\gamma),\\ \\forall g:\\mathrm{BoundedLatticeHom}(\\alpha,\\beta),\\ f\\circ g \\in \\mathrm{BoundedLatticeHom}(\\alpha,\\gamma)$$$

Lean4

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

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