property — Mathlib

English

If a morphism f: X → Y satisfies P.relative F, then for any pullback situation with X' → X, the corresponding pulled-back morphism snd satisfies P.

Русский

Если морфизм f: X → Y удовлетворяет P.relative F, то в любой ситуации вытяжки с X' → X соответствующий вытянутый морфизм snd удовлетворяет P.

LaTeX

$$$\forall a,b:\;g:\ F(a)\to Y,\; fst:\ F(b)\to X,\; snd:\;b\to a,\; IsPullback(fst, F(snd), f, g)\Rightarrow P(snd)$$$

Lean4

theorem property {f : X ⟶ Y} (hf : P.relative F f) :
    ∀ ⦃a b : C⦄ (g : F.obj a ⟶ Y) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : IsPullback fst (F.map snd) f g), P snd :=
  hf.2

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