π_arrow — Mathlib

English

For every index j in J, the projection π arrows j composed with the corresponding arrow equals the base map: π arrows j ≫ arrows j = base arrows.

Русский

Для каждого j ∈ J композиция π arrows j с arrows j равна базовой стрелке: π arrows j ≫ arrows j = base arrows.

LaTeX

$$$\\pi\\text{ arrows } j \\;\\circ\\; arrows_j = \\text{base arrows}$ for all j ∈ J.$$

Lean4

@[reassoc (attr := simp)]
theorem π_arrow (j : J) : π arrows j ≫ arrows _ = base arrows := by
  apply limit.w (WidePullbackShape.wideCospan _ _ _) (WidePullbackShape.Hom.term j)

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