nhdsGE_eq_iInf_principal — Mathlib

English

Dual formulation of the previous relation: the neighborhood filter above a equals the infimum of principal filters of initial intervals in the dual order.

Русский

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

LaTeX

$$$\\text{nhdsAbove}(a) = \\operatorname{Inf}_{u>a} \\mathcal{P}(I(a,u)).$$$

Lean4

theorem nhdsGE_eq_iInf_principal [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α} (ha : ∃ u, a < u) :
    𝓝[≥] a = ⨅ (u) (_ : a < u), 𝓟 (Ico a u) := by
  simp only [nhdsGE_eq_iInf_inf_principal, biInf_inf ha, inf_principal, Iio_inter_Ici]

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