ofHom_comp — Mathlib

English

OfHom preserves composition: for f: X →o Y and g: Y →o Z, we have ofHom(g ∘ f) = ofHom(f) ≫ ofHom(g).

Русский

OfHom сохраняет композицию: для f: X →o Y и g: Y →o Z верно, что ofHom(g ∘ f) = ofHom(f) ≫ ofHom(g).

LaTeX

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

Lean4

@[simp]
theorem ofHom_comp {X Y Z : Type u} [Preorder X] [Preorder Y] [Preorder Z] (f : X →o Y) (g : Y →o Z) :
    ofHom (g.comp f) = ofHom f ≫ ofHom g :=
  rfl

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