instFibrationFstOfIsFibrant — Mathlib

English

If Y is fibrant and X,Y have terminal/base-change properties, then prod.fst is a fibration.

Русский

Если Y фибривант и существуют соответствующие свойства термина/базового изменения, тогда prod.fst — фибрация.

LaTeX

$$$\text{Fibration}(\mathrm{prod.fst})$$$

Lean4

instance [hY : IsFibrant Y] : Fibration (prod.fst : X ⨯ Y ⟶ X) :=
  by
  rw [isFibrant_iff] at hY
  rw [fibration_iff] at hY ⊢
  exact
    MorphismProperty.of_isPullback
      (IsPullback.of_isLimit_binaryFan_of_isTerminal (limit.isLimit (pair X Y)) terminalIsTerminal).flip hY

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