withTop_comp — Mathlib

English

Top-extension commutes with composition of LatticeHom maps.

Русский

Расширение вверх совместимо с композицией отображений гомоморфизмов решёток.

LaTeX

$$$ (f.{\mathrm{comp}} g).{\mathrm{withTop}} = f.{\mathrm{withTop}}.{\mathrm{comp}} g.{\mathrm{withTop}} $$$

Lean4

@[simp]
theorem withTop_comp (f : LatticeHom β γ) (g : LatticeHom α β) : (f.comp g).withTop = f.withTop.comp g.withTop :=
  DFunLike.coe_injective <| Eq.symm <| WithTop.map_comp_map _ _

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