image_comp — Mathlib

English

Let G be a subpresheaf of F and f: F → F' and g: F' → F''. Then the image of the composite under g equals the image under g of the image under f.

Русский

Пусть G — подпрефеш F, и f: F → F', g: F' → F''. Тогда образ композиции f ≫ g равен образу g от образа f.

LaTeX

$$$ G.\\mathrm{image}(f \\circ g) = (G.\\mathrm{image} f).\\mathrm{image} g $$$

Lean4

theorem image_comp (g : F' ⟶ F'') : G.image (f ≫ g) = (G.image f).image g := by aesop

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