English
Let X be a scheme, U ⊆ X open, f ∈ Γ(X,U), and x ∈ X. The point x lies in the basic open X.basicOpen f if and only if there exists some witness m that certifies x ∈ U such that the germ of f at x with respect to m is a unit.
Русский
Пусть X — схема, U ⊆ X открыто, f — секция над U, и x ∈ X. Точка x принадлежит базовому открытому X.basicOpen(f) тогда, когда существует некое доказательство m, подтверждающее, что x ∈ U, такое что герм f в x по m является единицей.
LaTeX
$$$x \\in X.basicOpen f \\iff \\exists m\\; (m: x \\in U),\\; \\operatorname{IsUnit}\\left( X.presheaf.germ U x m f\\right)$$$
Lean4
/-- A variant of `mem_basicOpen` without the `x ∈ U` assumption. -/
theorem mem_basicOpen'' {U : X.Opens} (f : Γ(X, U)) (x : X) :
x ∈ X.basicOpen f ↔ ∃ (m : x ∈ U), IsUnit (X.presheaf.germ U x m f) :=
Iff.rfl
