English
If the germ of a section at x is zero, then there is a neighborhood V of x and a morphism mapping f to zero on V.
Русский
Если топологический росток секции в точке x равен нулю, то существует окрестность V точки x и отображение, переводящее f в ноль на V.
LaTeX
$$$\exists V, i: V \to U, x \in V, (f|_V) = 0$$$
Lean4
/-- If the germ of a section `f` is zero in the stalk at `x`, then `f` is zero on some neighbourhood
around `x`. -/
theorem exists_res_eq_zero_of_germ_eq_zero (U : Opens X) (f : X.presheaf.obj (op U)) (x : U)
(h : X.presheaf.germ U x.val x.property f = 0) :
∃ (V : Opens X) (i : V ⟶ U) (_ : x.1 ∈ V), X.presheaf.map i.op f = 0 :=
by
have h1 : X.presheaf.germ U x.val x.property f = X.presheaf.germ U x.val x.property 0 := by simpa
obtain ⟨V, hv, i, _, (hv4 : (X.presheaf.map i.op) f = (X.presheaf.map _) 0)⟩ :=
TopCat.Presheaf.germ_eq X.presheaf x.1 x.2 x.2 f 0 h1
use V, i, hv
simpa using hv4
