isOpenEmbedding_isZariskiLocalAtTarget

English

The property of being an open embedding is Zariski-local on the target.

Русский

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

LaTeX

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

Lean4

instance isOpenEmbedding_isZariskiLocalAtTarget : IsZariskiLocalAtTarget (topologically IsOpenEmbedding) :=
  topologically_isZariskiLocalAtTarget' _ fun _ _ _ hU ↦ hU.isOpenEmbedding_iff_restrictPreimage

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