isClosedEmbedding_isZariskiLocalAtTarget

English

The property of being a closed embedding is Zariski-local on the target.

Русский

Свойство быть закрытым вложением локально по Зариски на мишени.

LaTeX

$$$IsZariskiLocalAtTarget(\text{topologically IsClosedEmbedding})$$$

Lean4

instance isClosedEmbedding_isZariskiLocalAtTarget : IsZariskiLocalAtTarget (topologically IsClosedEmbedding) :=
  topologically_isZariskiLocalAtTarget' _ fun _ _ _ hU ↦ hU.isClosedEmbedding_iff_restrictPreimage

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