nhdsLE_eq_iInf_inf_principal — Mathlib

English

In a topological space with a preorder and order topology, the neighborhood filter above a equals the infimum over all larger elements of principal filters of initial intervals.

Русский

В топологическом пространстве с порядком и порядковой топологией окрестности от a сверху равны инфимума над всеми большими элементами над a их простыми фильтрами начальных интервалов.

LaTeX

$$$\\mathcal{N}_{\\ge a} = \\bigwedge_{u>a} \\mathcal{P}(I_{0}(a,u)).$$$

Lean4

theorem nhdsLE_eq_iInf_inf_principal [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
    𝓝[≤] a = (⨅ l < a, 𝓟 (Ioi l)) ⊓ 𝓟 (Iic a) :=
  nhdsGE_eq_iInf_inf_principal (toDual a)

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