mem_basicOpen_top — Mathlib

English

If f is a section of the structure sheaf over the top open ⊤, then a point x ∈ X belongs to the basic open X.basicOpen f exactly when the germ of f at x (in the top stalk) is a unit.

Русский

Если f является секцией над верхним открытым ⊤, то точка x принадлежит базовому открытому X.basicOpen(f) тогда и только тогда, когда герм f в x (в пучке над x) является единицей.

LaTeX

$$$x \\in X.basicOpen f \\iff \\operatorname{IsUnit}\\left( X.presheaf.germ \\top x \\text{trivial} f\\right)$$$

Lean4

@[simp]
theorem mem_basicOpen_top (f : Γ(X, ⊤)) (x : X) : x ∈ X.basicOpen f ↔ IsUnit (X.presheaf.germ ⊤ x trivial f) :=
  RingedSpace.mem_top_basicOpen _ f x

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