mkPrecomp_comp — Mathlib

English

mkPrecomp f (g' ∘ g) = eqToHom (by simp) ∘ mkPrecomp (S.map g ∘ f) g' ∘ mkPrecomp f g.

Русский

mkPrecomp f (g' ∘ g) = eqToHom (by simp) ∘ mkPrecomp (S.map g ∘ f) g' ∘ mkPrecomp f g.

LaTeX

$$$\\mathrm{mkPrecomp}\\, f\\, (g' \\circ g) = \\mathrm{eqToHom}(\\text{by simp}) \\circ \\mathrm{mkPrecomp}(S.map g \\circ f)\\, g' \\circ \\mathrm{mkPrecomp}\\, f\\, g$$$

Lean4

theorem mkPrecomp_comp (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) (g' : Y'' ⟶ Y') :
    mkPrecomp f (g' ≫ g) = eqToHom (by simp) ≫ mkPrecomp (S.map g ≫ f) g' ≫ mkPrecomp f g := by simp

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