isPullback' — Mathlib

English

With Full F, IsPullback (F.map (hf'.fst' g)) (F.map (hf'.snd g)) f' g.

Русский

При условии полноты F: IsPullback( F.map (hf'.fst' g), F.map (hf'.snd g), f', g).

LaTeX

$$$ IsPullback (F.map (hf'.fst' g)) (F.map (hf'.snd g)) f' g $$$

Lean4

/-- Variant of the pullback square when `F` is full, and given `f' : F.obj b ⟶ Y`. -/
theorem isPullback' [Full F] : IsPullback (F.map (hf'.fst' g)) (F.map (hf'.snd g)) f' g :=
  (hf'.map_fst' _) ▸ hf'.isPullback g

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