nhdsOrderEmbedding — Mathlib

English

The neighborhood filter map gives an order-embedding of PrimeSpectrum(R) into the lattice of filters on PrimeSpectrum(R).

Русский

Картина локальных окрестностей задаёт вложение по порядку PrimeSpectrum(R) в решётку фильтров на PrimeSpectrum(R).

LaTeX

$$$$ \mathrm{nhdsOrderEmbedding} : \operatorname{PrimeSpectrum}(R) \hookrightarrow_{\text{order}} \operatorname{Filter}( \operatorname{PrimeSpectrum}(R) ). $$$$

Lean4

/-- `nhds` as an order embedding. -/
@[simps!]
def nhdsOrderEmbedding : PrimeSpectrum R ↪o Filter (PrimeSpectrum R) :=
  OrderEmbedding.ofMapLEIff nhds fun a b => (le_iff_specializes a b).symm

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