nhdsGE — Mathlib

English

In a SuccOrder, the upper neighborhood filter at any element a is the principal filter at a; i.e., 𝓝[≥] a = pure a for all a.

Русский

В упорядоченном по сучке (SuccOrder) пространстве окрестности сверху для любого a совпадают с главной фильтром по a; то есть 𝓝[≥] a = pure a для всех a.

LaTeX

$$$\forall a\, 𝓝_{\ge a}(a) = \mathrm{pure}(a)$$$

Lean4

protected theorem nhdsGE [SuccOrder α] : 𝓝[≥] a = pure a :=
  PredOrder.nhdsLE (α := αᵒᵈ)

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