evaluation_ne_zero_iff_mem_basicOpen

English

The evaluation is nonzero precisely when the point lies in the basic open.

Русский

Значение оценки не нулевое тогда и только тогда, когда точка лежит в базовом открытом.

LaTeX

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

Lean4

theorem evaluation_ne_zero_iff_mem_basicOpen (x : X) (hx : x ∈ U) (f : Γ(X, U)) :
    X.evaluation U x hx f ≠ 0 ↔ x ∈ X.basicOpen f := by simp

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