evaluation_eq_zero_iff_notMem_basicOpen

English

The basic open is empty iff every evaluation at every point is zero.

Русский

Базовое открытое множество равно пустому множеству тогда и только тогда, когда всякие значения равны нулю.

LaTeX

$$$$ X.\mathrm{basicOpen}(f) = \emptyset \iff \forall x \in U, X.\mathrm{evaluation}(U, x, hx, f) = 0. $$$$

Lean4

@[simp]
theorem evaluation_eq_zero_iff_notMem_basicOpen (x : X) (hx : x ∈ U) (f : Γ(X, U)) :
    X.evaluation U x hx f = 0 ↔ x ∉ X.basicOpen f :=
  X.toLocallyRingedSpace.evaluation_eq_zero_iff_notMem_basicOpen ⟨x, hx⟩ f

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