image_comap_C_basicOpen — Mathlib

English

For a polynomial f, the comap image of basicOpen f coincides with the complement of the zero locus of the range of f.

Русский

Образ comap basicOpen f совпадает с дополнением нулевой локусы множества коэффициентов f.

LaTeX

$$$x \\in\\text{comap }C '' \\text{basicOpen}(f) \\iff x \\in (\\text{zeroLocus}(\\{\\text{coeff}(f,i) : i\\in\\mathbb{N}\\}))^c$$$

Lean4

theorem image_comap_C_basicOpen (f : R[X]) : comap C '' basicOpen f = (zeroLocus (Set.range f.coeff))ᶜ :=
  by
  ext p
  rw [mem_image_comap_C_basicOpen]
  simp [Set.range_subset_iff]

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