w — Mathlib · SciLib

English

The equality w expresses compatibility of the pullback arrows, ensuring the left map equals the right maps composed with fork components.

Русский

Выражение совместимости стрел-обратных диаграмм = равенство левой карты и правых карт композициями вилки.

LaTeX

$$$\text{w} : \text{forkMap } P X π \;\text{≫ firstMap } P X π = \text{forkMap } P X π \;\text{≫ secondMap } P X π$$$

Lean4

theorem w : forkMap P X π ≫ firstMap P X π = forkMap P X π ≫ secondMap P X π :=
  by
  ext x ij
  simp only [firstMap, secondMap, forkMap, types_comp_apply, Types.pi_lift_π_apply, ← FunctorToTypes.map_comp_apply,
    ← op_comp, pullback.condition]

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