pullback_fst_iff — Mathlib

English

Under base-change stability and descent along Q, with HasPullback, the pullback left leg satisfies P if and only if the other leg satisfies P, given hf.

Русский

При устойчивости к базовым изменениям и спуску по Q, наличие P на fst эквивалентно наличию P на g при HasPullback и hf.

LaTeX

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

Lean4

theorem pullback_fst_iff [P.IsStableUnderBaseChange] [P.DescendsAlong Q] [HasPullback f g] (hf : Q f) :
    P (pullback.fst f g) ↔ P g :=
  iff_of_isPullback (.of_hasPullback f g) hf

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