nhdsWithin_neBot — Mathlib

English

If a is the least upper bound of a nonempty set s, then the neighborhood filter within s at a is nontrivial.

Русский

Если a является наименьшей верхней границей непустого множества s, то фильтр окрестностей внутри s в точке a не тривиален.

LaTeX

$$$IsLUB\\,s\\,a \\rightarrow s \\neq \\varnothing \\rightarrow (nhdsWithin\\,a\\,s).NeBot$$$

Lean4

theorem nhdsWithin_neBot {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : NeBot (𝓝[s] a) :=
  mem_closure_iff_nhdsWithin_neBot.1 (ha.mem_closure hs)

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