map_p₃_comp

Mathlib.CategoryTheory.MorphismProperty.Representable

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.relativelyRepresentable.pullback₃.map_p₃_comp

English

Similarly, F.map(p3) ∘ f3 equals π in the pullback₃ construction.

Русский

Аналогично, F.map(p3) ∘ f3 равно π в конструировании pullback₃.

LaTeX

$$$F.map(p_3(\dots)) \;\circ f_3 = \pi_{\dots}$$$

Lean4

@[reassoc (attr := simp)]
theorem map_p₃_comp : F.map (p₃ hf₁ f₂ f₃) ≫ f₃ = π _ _ _ := by simp [π, p₁, p₃, ← hf₁.w f₃, pullback.condition]

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

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

Разделы

Аффилиация

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