ofHom_comp — Mathlib

English

ofHom preserves composition: ofHom(g ∘ f) = ofHom(f) ≫ ofHom(g).

Русский

ofHom сохраняет композицию: ofHom(g ∘ f) = ofHom(f) ≫ ofHom(g).

LaTeX

$$$$ \operatorname{ofHom}(g \circ f) = \operatorname{ofHom}(f) \circ \operatorname{ofHom}(g). $$$$

Lean4

@[simp]
theorem ofHom_comp {X Y Z : Type u} [DistribLattice X] [BoundedOrder X] [Fintype X] [DistribLattice Y] [BoundedOrder Y]
    [Fintype Y] [DistribLattice Z] [BoundedOrder Z] [Fintype Z] (f : BoundedLatticeHom X Y)
    (g : BoundedLatticeHom Y Z) : ofHom (g.comp f) = ofHom f ≫ ofHom g :=
  rfl

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