pasteHoriz

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

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

Lean4

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

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

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

Разделы

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

Аффилиация

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