restrict — Mathlib

English

If a morphism f has property P and U is an affine open in Y, then the restricted morphism f|_U has property Q.

Русский

Если морфизм f удовлетворяет свойству P, и U — аффинное открытое множество в Y, то ограничение f на U имеет свойство Q.

LaTeX

$$$\forall f:X\to Y,\; P f \Rightarrow \forall U\in Y\text{ aff.opens},\; Q(f\big|_{U})$$$

Lean4

theorem restrict (hf : P f) (U : Y.affineOpens) : Q (f ∣_ U) :=
  of_isPullback (isPullback_morphismRestrict f U).flip hf

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