coe_comp_sup_hom — Mathlib

English

Composition of lattice homomorphisms, seen as SupHom, matches the SupHom composition.

Русский

Композиция гомоморфизмов решетки, рассматриваемая как SupHom, совпадает с их композицией в SupHom.

LaTeX

$$$(f.comp g : SupHom \alpha \gamma) = (f : SupHom \beta \gamma).comp g$$$

Lean4

theorem coe_comp_sup_hom (f : LatticeHom β γ) (g : LatticeHom α β) :
    (f.comp g : SupHom α γ) = (f : SupHom β γ).comp g :=
  rfl

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