of_comp_finiteType — Mathlib

English

If the composition (g ∘ f) is finitely presented and f is of finite type, then g is finitely presented.

Русский

Если композиция g∘f конечнопредставима, а f имеет конечную презентацию, то и g конечнопредставим.

LaTeX

$$$ (g\\circ f).FinitePresentation \\land f.FiniteType \\Rightarrow g.FinitePresentation $$$

Lean4

nonrec theorem of_comp_finiteType (f : A →ₐ[R] B) {g : B →ₐ[R] C} (h : (g.comp f).FinitePresentation)
    (h' : f.FiniteType) : g.FinitePresentation :=
  h.of_comp_finiteType _ h'

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