preimage_basicOpen — Mathlib

English

Restricting the section f to a subopen yields a basic open that is contained in the original basic open.

Русский

Ограничение секции f до суб-открытого даёт базовое открытое, входящее в исходное базовое открытое.

LaTeX

$$$X.basicOpen\\left(TopCat.Presheaf.restrict f i\\right) \\le X.basicOpen f$$$

Lean4

@[simp]
theorem preimage_basicOpen {X Y : Scheme.{u}} (f : X ⟶ Y) {U : Y.Opens} (r : Γ(Y, U)) :
    f ⁻¹ᵁ (Y.basicOpen r) = X.basicOpen (f.app U r) :=
  LocallyRingedSpace.preimage_basicOpen f.toLRSHom r

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