withBot_comp — Mathlib

English

The withBot extension preserves composition: the withBot of a composite equals the composite of withBot extensions.

Русский

Расширение WithBot сохраняет композицию: withBot от композиции равен композиции withBot применений.

LaTeX

$$$ (f \\circ g).\\mathrm{withBot} = f.\\mathrm{withBot} \\circ g.\\mathrm{withBot} $$$

Lean4

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

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