isBounded_le_nhds — Mathlib

English

For any a in a topological space with bounded LENhds, the neighborhood 𝓝(a) is bounded from above with respect to ≤.

Русский

Для любой точки a в топологическом пространстве с ограниченным LENhds множество окрестностей ограничено сверху по ≤.

LaTeX

$$$$ (\mathcal{N}a).IsBounded(\cdot \le \cdot). $$$$

Lean4

theorem isBounded_le_nhds (a : α) : (𝓝 a).IsBounded (· ≤ ·) :=
  BoundedLENhdsClass.isBounded_le_nhds _

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