fromIncl_asSigma

Mathlib.CategoryTheory.Limits.FormalCoproducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl_asSigma

English

A morphism from Incl X to Y is determined by its sigma pair (fst,snd).

Русский

Морфизм из Incl X в Y задаётся парой (fst,snd).

LaTeX

$$$\\mathrm{Hom.fromIncl}(f.1,f.2)=f$$$

Lean4

theorem fromIncl_asSigma (f : (incl C).obj X ⟶ Y) : Hom.fromIncl f.asSigma.fst f.asSigma.snd = f := by ext <;> aesop

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

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

Разделы

Аффилиация

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