basicOpen — Mathlib

English

The basic open subset defined by a section f is the locus where f does not vanish.

Русский

Базовое открытое множество, задаваемое секцией f, является множеством точек, где f не обращается нулю.

LaTeX

$$$ \mathrm{basicOpen}_X(f) = \{ x \in X \mid \text{the germ of } f \text{ at } x \text{ is nonvanishing} \}$$$

Lean4

/-- The subset of the underlying space where the given section does not vanish. -/
def basicOpen : X.Opens :=
  X.toLocallyRingedSpace.toRingedSpace.basicOpen f

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