coe_comp_sup_hom' — Mathlib

English

A simp-normal form equality: the pair (f ∘ g, map_sup (f.comp g)) equals the SupHom composition.

Русский

Упрощенное равенство: пара (f∘g, map_sup (f∘g)) равна композиции SupHom.

LaTeX

$$$\langle f \circ g, \operatorname{map\_sup}(f.comp g)\rangle = (f : SupHom \beta \gamma).comp g$$$

Lean4

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

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

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