le_iff_specializes — Mathlib

English

In the Zariski topology on PrimeSpectrum(R), x ≤ y if and only if x specializes to y.

Русский

В топологии Зарици на PrimeSpectrum(R) выполняется: x ≤ y тогда и только тогда x специализируется на y.

LaTeX

$$$$ x \le y \iff x \rightsquigarrow y. $$$$

Lean4

theorem le_iff_specializes (x y : PrimeSpectrum R) : x ≤ y ↔ x ⤳ y :=
  (le_iff_mem_closure x y).trans specializes_iff_mem_closure.symm

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