mkHom_comp — Mathlib

English

If f and g are NormNoninc, then mkHom (g ∘ f) hgf equals mkHom f hf ≫ mkHom g hg.

Русский

Если f и g NormNoninc, то mkHom (g ∘ f) hgf равно mkHom f hf затем состав mkHom g hg.

LaTeX

$$$ mkHom (g \circ f) hgf = mkHom f hf \\;\; \circ mkHom g hg $$$

Lean4

@[simp]
theorem mkHom_comp {M N O : Type u} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] [SeminormedAddCommGroup O]
    (f : NormedAddGroupHom M N) (g : NormedAddGroupHom N O) (hf : f.NormNoninc) (hg : g.NormNoninc)
    (hgf : (g.comp f).NormNoninc) : mkHom (g.comp f) hgf = mkHom f hf ≫ mkHom g hg :=
  rfl

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