fromSpec_preimage_basicOpen — Mathlib

English

In the same setting, the preimage of a basic open is a basic open: explicit equality with basicOpen f.

Русский

В той же постановке предобраз базовой области является базовой областью: явное равенство с basicOpen f.

LaTeX

$$$h_U.fromSpec^{-1} X.basicOpen f = \mathrm{PrimeSpectrum.basicOpen} f$$$

Lean4

theorem fromSpec_preimage_basicOpen : hU.fromSpec ⁻¹ᵁ X.basicOpen f = PrimeSpectrum.basicOpen f := by
  rw [fromSpec_preimage_basicOpen', ← basicOpen_eq_of_affine]

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