English
If P is local at source and target, and stable under postcomposition with open immersions, then P is local at the target; more precisely, P can be checked after composing with open immersions and pulling back along pullbacks.
Русский
Если P локально по источнику и цели и стабильно при посткомпозиции с открытыми вложениями, то P локально по цели; точнее, проверка выполняется после композиции с открытыми вложениями и вытягиванием через тягосоглашения.
LaTeX
$$$[P.IsMultiplicative] \to IsZariskiLocalAtTarget P$, with hypotheses as in the text.$$
Lean4
/-- If `P` is local at the source and the target, then restriction on both source and target
preserves `P`. -/
theorem resLE [IsZariskiLocalAtTarget P] {U : Y.Opens} {V : X.Opens} (e : V ≤ f ⁻¹ᵁ U) (hf : P f) : P (f.resLE U V e) :=
IsZariskiLocalAtSource.comp (IsZariskiLocalAtTarget.restrict hf U) _
