nhdsGT_neBot — Mathlib

English

Given a ≤ b in a densely ordered topological space, the neighborhood system to the right of a inside Ioi a toward b is nonempty.

Русский

При a ≤ b в плотно упорядоченном топологическом пространстве правая окрестность внутри Ioi(a) ненулевая.

LaTeX

$$$\text{nhdsWithin}(b, \mathrm{Ioi}(a)) \text{ is NeBot when } a \le b$$$

Lean4

instance nhdsGT_neBot [NoMaxOrder α] (a : α) : NeBot (𝓝[>] a) :=
  nhdsWithin_Ioi_neBot le_rfl

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