coe_comp_lattice_hom — Mathlib

English

The lattice-homomorphism part of a composed bounded lattice homomorphism equals the composition of the lattice-homomorphism parts (primed form).

Русский

Часть, отвечающая за решетку, состава ограниченного гомоморфизма равна композиции соответствующих частей (первичная форма).

LaTeX

$$$ (f.comp g : \\mathrm{LatticeHom}(\\alpha, \\gamma)) = (f : \\mathrm{LatticeHom}(\\beta, \\gamma)).comp g $$$

Lean4

theorem coe_comp_lattice_hom (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
    (f.comp g : LatticeHom α γ) = (f : LatticeHom β γ).comp g :=
  rfl

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