hasPullback_of_preservesPullback — Mathlib

English

If G preserves a pullback for f and g and C has a pullback, then the pushforward F maps yield a pullback in D.

Русский

Если в C есть притяжение для f,g и G сохраняет притяжение, то G отображает притяжение в D.

LaTeX

$$$HasPullback( G.map f, G.map g )$$$

Lean4

theorem hasPullback_of_preservesPullback [HasPullback f g] : HasPullback (G.map f) (G.map g) :=
  ⟨⟨⟨_, isLimitPullbackConeMapOfIsLimit G _ (pullbackIsPullback _ _)⟩⟩⟩

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