basicOpen_eq_bot_iff_forall_evaluation_eq_zero

English

For a presheaf section f on U, the basic open equals the bottom open if and only if every point x in U evaluates to zero on f.

Русский

Для секции f над U базовый открытый множество совпадает с нулём (⊥) тогда и только тогда, когда для каждого x ∈ U значение evaluation x f равно 0.

LaTeX

$$$ X.\\mathrm{toRingedSpace}.basicOpen\\, f = \\bottom \\iff \\forall x : U,\\ X.\\mathrm{evaluation}\\, x\\, f = 0 $$$

Lean4

theorem basicOpen_eq_bot_iff_forall_evaluation_eq_zero (f : X.presheaf.obj (op U)) :
    X.toRingedSpace.basicOpen f = ⊥ ↔ ∀ (x : U), X.evaluation x f = 0 :=
  by
  simp only [evaluation_eq_zero_iff_notMem_basicOpen, Subtype.forall]
  exact ⟨fun h ↦ h ▸ fun a _ hc ↦ hc, fun h ↦ eq_bot_iff.mpr <| fun a ha ↦ h a (X.toRingedSpace.basicOpen_le f ha) ha⟩

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