basicOpen_res — Mathlib

English

Given a morphism i : op U ⟶ op V between opens, the basic open of the pullback of f along i equals the intersection of V with the basic open of f.

Русский

Если есть гомоморфизм ограничений i : op U ⟶ op V между открытыми, то базовое открытое для вытянутого по i f равно пересечению V с базовым открытым для f.

LaTeX

$$$X.basicOpen\\left( X.presheaf.map i\\, f\\right) = V \\cap X.basicOpen f$$$

Lean4

@[simp]
theorem basicOpen_res (i : op U ⟶ op V) : X.basicOpen (X.presheaf.map i f) = V ⊓ X.basicOpen f :=
  RingedSpace.basicOpen_res _ i f

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