le_iff_mem_closure — Mathlib

English

The order relation can be read as closure of a singleton: x ≤ y iff y belongs to the closure of {x}.

Русский

Отношение порядка читается как замыкание одиничного множества: x ≤ y тогда и только тогда, когда y принадлежит замыканию {x}.

LaTeX

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

Lean4

theorem le_iff_mem_closure (x y : ProjectiveSpectrum 𝒜) : x ≤ y ↔ y ∈ closure ({ x } : Set (ProjectiveSpectrum 𝒜)) :=
  by
  rw [← as_ideal_le_as_ideal, ← zeroLocus_vanishingIdeal_eq_closure, mem_zeroLocus, vanishingIdeal_singleton]
  simp only [as_ideal_le_as_ideal, coe_subset_coe]

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