nhdsWithin_neBot — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem nhdsWithin_neBot {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) : NeBot (𝓝[s] a) :=
  IsLUB.nhdsWithin_neBot (α := αᵒᵈ) ha hs

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