pasteVert

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

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

Lean4

/-- The `PullbackCone` obtained by pasting two `PullbackCone`'s vertically -/
abbrev pasteVert (t₁ : PushoutCocone g₂ i₃) {i₂ : Y₂ ⟶ t₁.pt} (t₂ : PushoutCocone g₁ i₂) (hi₂ : i₂ = t₁.inl) :
    PushoutCocone (g₂ ≫ g₁) i₃ :=
  PushoutCocone.mk t₂.inl (t₁.inr ≫ t₂.inr) (by rw [← reassoc_of% t₁.condition, Category.assoc, t₂.condition, ← hi₂])

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

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

Разделы

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

Аффилиация

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