ofHom_comp — Mathlib

English

Let f : X → Y and g : Y → Z be FrameHoms. Then Frm.ofHom respects composition: the image of g ∘ f is the composition of Frm.ofHom f and Frm.ofHom g.

Русский

Пусть f : X → Y и g : Y → Z — гомоморфизмы рамок. Тогда Frm.ofHom сохраняет композицию: Frm.ofHom( g ∘ f ) = Frm.ofHom(f) ∘ Frm.ofHom(g).

LaTeX

$$$ \mathrm{ofHom}(g \circ f) = \mathrm{ofHom}(f) \circ \mathrm{ofHom}(g) $$$

Lean4

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

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