coe_comp_sup_hom' — Mathlib

English

The SupHom part of a bounded lattice homomorphism composes with g as a SupHom.

Русский

Часть SupHom композиции ограниченного гомоморфизма образует SupHom композицию с g.

LaTeX

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

Lean4

@[simp]
  -- `simp`-normal form of `coe_comp_sup_hom`

theorem coe_comp_sup_hom' (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
    ⟨f ∘ g, map_sup (f.comp g)⟩ = (f : SupHom β γ).comp g :=
  rfl

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