nhdsGE — Mathlib

English

Let a and b be elements of a linearly ordered space with ClosedIciTopology. If a is covered by b, then the upper neighborhood filter at a collapses to the principal filter at a; i.e., there are no nontrivial neighborhoods of a from above.

Русский

Пусть a и b — элементы упорядоченного пространства с замкнутой топологией по верхней границе. Если a покрывается b, то окрестности сверху в a тривиальны: 𝓝[≥] a = {a}.

LaTeX

$$$\forall a,b\, (a \;\triangleleft\; b) \Rightarrow \ nhdsWithin a (\{x \mid a \le x\}) = \mathrm{pure}(a)$$$

Lean4

protected theorem nhdsGE (H : a ⋖ b) : 𝓝[≥] a = pure a :=
  H.toDual.nhdsLE

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