instIsOpenImmersionHomOfLE — Mathlib

English

Let X be a scheme and U ≤ V be opens of X. Then the natural morphism X.homOfLE e: U → V induces an open immersion of schemes, i.e., the morphism X.homOfLE e is an open immersion.

Русский

Пусть X — схема, и U ⊆ V — открытые подмножества X. Тогда отображение X.homOfLE e: U → V является открытым внедрением между схемами.

LaTeX

$$$\\operatorname{IsOpenImmersion}(X.homOfLE(e))$$$

Lean4

instance (X : Scheme.{u}) {U V : X.Opens} (e : U ≤ V) : IsOpenImmersion (X.homOfLE e) :=
  by
  delta Scheme.homOfLE
  infer_instance

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