coe_comp_inf_hom' — Mathlib

English

The InfHom analogue: the pair (f ∘ g, map_inf (f.comp g)) equals the InfHom composition.

Русский

Аналогично InfHom: пара (f∘g, map_inf (f∘g)) совпадает с композицией InfHom.

LaTeX

$$$\langle f \circ g, \operatorname{map\_inf}(f.comp g)\rangle = (f : InfHom \alpha \gamma).comp g$$$

Lean4

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

theorem coe_comp_inf_hom' (f : LatticeHom β γ) (g : LatticeHom α β) :
    ⟨f ∘ g, map_inf (f.comp g)⟩ = (f : InfHom β γ).comp g :=
  rfl

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