basicOpen_zero — Mathlib

English

For any Locally Ringed Space X and any open U, the basic open defined by the zero section is the bottom element, i.e., the empty open set.

Русский

Для локально кольцевого пространства X и любого открытого множества U базовое открытое, задаваемое нулевой секцией, равно нижнему элементу, то есть пустому открытому множеству.

LaTeX

$$$$X^{\\mathrm{toRingedSpace}}.\\mathrm{basicOpen}(0) = \\bot.$$$$

Lean4

theorem basicOpen_zero (X : LocallyRingedSpace.{u}) (U : Opens X.carrier) :
    X.toRingedSpace.basicOpen (0 : X.presheaf.obj <| op U) = ⊥ :=
  by
  ext x
  simp only [RingedSpace.basicOpen, Opens.coe_mk, Set.mem_setOf_eq, Opens.coe_bot, Set.mem_empty_iff_false, iff_false,
    not_exists]
  intro hx
  rw [map_zero, isUnit_zero_iff]
  change (0 : X.presheaf.stalk x) ≠ (1 : X.presheaf.stalk x)
  exact zero_ne_one

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