pullback_fst — Mathlib

English

If the base-change stability holds, then the pullback fst map preserves the property P when g is given.

Русский

При условии устойчивости к базовому изменению отображение fst pullback сохраняет свойство P при заданном g.

LaTeX

$$P (pullback.fst f g)$$

Lean4

theorem pullback_fst [IsStableUnderBaseChange P] {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [HasPullback f g] (H : P g) :
    P (pullback.fst f g) :=
  of_isPullback (IsPullback.of_hasPullback f g).flip H

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