instIsZariskiLocalAtSource — Mathlib

English

UniversallyOpen is a Zariski-local property on the source: if a morphism is universally open after restricting to a Zariski cover of the source, then it is universally open.

Русский

Sвойство УниверсальноОткрыто локально по источнику: если морфизм универсально открыт на открытом покрытии источника, то он таковым и является.

LaTeX

$$$\IsZariskiLocalAtSource(\mathsf{UniversallyOpen}).$$$

Lean4

instance : IsZariskiLocalAtSource @UniversallyOpen := by
  rw [eq]
  exact universally_isZariskiLocalAtSource _

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