isOpenMap_isZariskiLocalAtTarget — Mathlib

English

The property of being an open map is Zariski-local on the target; this can be verified after restricting to Zariski-open covers of the target.

Русский

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

LaTeX

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

Lean4

instance isOpenMap_isZariskiLocalAtTarget : IsZariskiLocalAtTarget (topologically IsOpenMap) :=
  topologically_isZariskiLocalAtTarget' _ fun _ _ _ hU _ ↦ hU.isOpenMap_iff_restrictPreimage

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