inr_fst'

Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsPushout.inr_fst'

← MathLib Explorer

English

For a bilimit b of X and Y, the square with inr and the left projection s.t. 0 on the bottom is a pushout.

Русский

Для билилимита b квадраты с inr и fst дают пушаут.

LaTeX

$$$\operatorname{IsPushout}(b.inr, 0, b.fst, 0)$$$

Lean4

theorem inr_fst' {b : BinaryBicone X Y} (h : b.IsBilimit) : IsPushout b.inr (0 : Y ⟶ 0) b.fst (0 : 0 ⟶ X) :=
  by
  refine of_top ?_ (by simp) (of_isBilimit h)
  simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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