property_snd — Mathlib

English

If f is relatively representable, then for any a and g: F.obj a → Y, the declared snd in the pullback diagram satisfies P.

Русский

Если f относительнo представимо, то для любого a и g: F.obj a → Y, соответствующий snd в диаграмме вытяжки удовлетворяет P.

LaTeX

$$$\forall a\; (g:\, F(a)\to Y),\; P( \text{hf.rep.snd } g)$$$

Lean4

theorem property_snd {f : X ⟶ Y} (hf : P.relative F f) {a : C} (g : F.obj a ⟶ Y) : P (hf.rep.snd g) :=
  hf.property g _ _ (hf.rep.isPullback g)

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