toΓSpecMapBasicOpen_eq — Mathlib

English

The canonical map on sections on the basic open induced from the adjunction agrees with the canonical basic open map in X.

Русский

Каноническое отображение секций на базовом открытом совпадает с каноническим отображением в X.

LaTeX

$$$X.toΓSpecMapBasicOpen(r) = X.toRingedSpace.basicOpen(r).$$$

Lean4

/-- The preimage is the basic open in `X` defined by the same element `r`. -/
theorem toΓSpecMapBasicOpen_eq : X.toΓSpecMapBasicOpen r = X.toRingedSpace.basicOpen r :=
  Opens.ext (X.toΓSpec_preimage_basicOpen_eq r)

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