isClosedMap_isZariskiLocalAtTarget

Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.isClosedMap_isZariskiLocalAtTarget

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

instance isClosedMap_isZariskiLocalAtTarget : IsZariskiLocalAtTarget (topologically IsClosedMap) :=
  topologically_isZariskiLocalAtTarget' _ fun _ _ _ hU _ ↦ hU.isClosedMap_iff_restrictPreimage

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru