basicOpen_restrict — Mathlib

English

If i is an isomorphism between opens, then the basic open defined via X.presheaf.map i f equals the basic open of f.

Русский

Если i — изоморфизм между открытыми, то базовое открытое, определяемое через X.presheaf.map i f, равно базовому открытому f.

LaTeX

$$$X.basicOpen\\left( X.presheaf.map i f\\right) = X.basicOpen f\\,\\; [IsIso\\ i]$$$

Lean4

@[sheaf_restrict]
theorem basicOpen_restrict (i : V ⟶ U) (f : Γ(X, U)) : X.basicOpen (TopCat.Presheaf.restrict f i) ≤ X.basicOpen f :=
  (Scheme.basicOpen_res _ _ _).trans_le inf_le_right

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