pullback_snd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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