map_pre — Mathlib

English

For HasLimitsOfShape K C, and α: F ⟶ G, E: K ⥤ J, we have: lim.map α ≫ limit.pre G E = limit.pre F E ≫ lim.map (whiskerLeft E α).

Русский

Пусть существует предел формы K в C и α: F ⟶ G. Тогда lim.map α ∘ limit.pre G E = limit.pre F E ∘ lim.map (whiskerLeft E α).

LaTeX

$$$\\lim.map \\alpha \\;\\gg\\; \\limit.pre G E = \\limit.pre F E \\gg \\lim.map (\\mathrm{whiskerLeft} E \\alpha)$$$

Lean4

theorem map_pre [HasLimitsOfShape K C] (E : K ⥤ J) :
    lim.map α ≫ limit.pre G E = limit.pre F E ≫ lim.map (whiskerLeft E α) :=
  by
  ext
  simp

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