range_comp

Mathlib.CategoryTheory.Subpresheaf.Image

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subpresheaf.range_comp

English

For a morphism f: F → F' and g: F' → F'', the range of the composite f ≫ g equals the image of f under g.

Русский

Для морфизма f: F → F' и g: F' → F'', область (range) композиции f ≫ g равна образу f под действием g.

LaTeX

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

Lean4

theorem range_comp (g : F' ⟶ F'') : range (f ≫ g) = (range f).image g := by aesop

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru