le_iff_mem_closure — Mathlib

English

In PrimeSpectrum(R), x ≤ y if and only if y lies in the closure of {x} in the Zariski topology.

Русский

В PrimeSpectrum(R) x ≤ y тогда и только тогда, когда y принадлежит замыканию множества {x} в топологии Зарици.

LaTeX

$$$$ x \le y \iff y \in \overline{\{x\}}. $$$$

Lean4

theorem le_iff_mem_closure (x y : PrimeSpectrum R) : x ≤ y ↔ y ∈ closure ({ x } : Set (PrimeSpectrum R)) := by
  rw [← asIdeal_le_asIdeal, ← zeroLocus_vanishingIdeal_eq_closure, mem_zeroLocus, vanishingIdeal_singleton,
    SetLike.coe_subset_coe]

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