inl_eq_inr_of_epi_eq

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.inl_eq_inr_of_epi_eq

English

If f is epi, then inl equals inr in the pushout cocone for (f,f).

Русский

Если f эпиморфизм, то в пушпоутах для (f,f) inl равно inr.

LaTeX

$$$t.inl = t.inr$ for $t$ a PushoutCocone f f with epi f$$

Lean4

theorem inl_eq_inr_of_epi_eq : pushout.inl f f = pushout.inr f f :=
  PushoutCocone.inl_eq_inr_of_epi_eq (getColimitCocone (span f f)).cocone

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

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

Разделы

Аффилиация

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