isEmbedding_isZariskiLocalAtTarget

English

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

Русский

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

LaTeX

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

Lean4

instance isEmbedding_isZariskiLocalAtTarget : IsZariskiLocalAtTarget (topologically IsEmbedding) :=
  topologically_isZariskiLocalAtTarget' _ fun _ _ _ hU ↦ hU.isEmbedding_iff_restrictPreimage

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