pullback_snd_iff — Mathlib

English

With IsStableUnderBaseChange and P.DescendsAlong Q and HasPullback, Qg implies P(pullback.snd f g) iff P f.

Русский

При устойчивости к базовым изменениям и descendsAlong(Q), HasPullback, hg: Qg, тогда P pullback.snd f g эквивалентно P f.

LaTeX

$$$ [P.IsStableUnderBaseChange] [P.DescendsAlong Q] [HasPullback f g] (hg : Q g) : P (pullback.snd f g) \\leftrightarrow P f.$$$

Lean4

theorem pullback_snd_iff [P.IsStableUnderBaseChange] [P.DescendsAlong Q] [HasPullback f g] (hg : Q g) :
    P (pullback.snd f g) ↔ P f :=
  iff_of_isPullback (IsPullback.of_hasPullback f g).flip hg

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