isCobounded_le_nhds — Mathlib

English

The neighborhood filter is cobounded with respect to ≤; equivalently, it is not too large in the ≤-direction.

Русский

Окрестности точки не выходят за пределы по отношению к ≤; фильтр окрестностей сходится к ограниченности снизу.

LaTeX

$$$ (a : α) \Rightarrow (\mathcal{N}a).IsCobounded (\le). $$$

Lean4

theorem isCobounded_le_nhds (a : α) : (𝓝 a).IsCobounded (· ≤ ·) :=
  (isBounded_ge_nhds a).isCobounded_flip

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