isOpen_imageOfDf — Mathlib

English

The image of a polynomial's coefficient criterion is an open set in Spec R.

Русский

Образ критерия коэффициентов полинома является открытым множеством в Spec R.

LaTeX

$$$\\text{isOpen}(\\text{imageOfDf}(f))$$$

Lean4

theorem isOpen_imageOfDf : IsOpen (imageOfDf f) :=
  by
  rw [imageOfDf, setOf_exists fun i (x : PrimeSpectrum R) => coeff f i ∉ x.asIdeal]
  exact isOpen_iUnion fun i => isOpen_basicOpen

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