frequently_nhds_mem — Mathlib

English

If a is an LUB of s and s is nonempty, then there are frequently points of s in the neighborhood of a from below.

Русский

Если a — наибольшая нижняя граница множества s и s непусто, то в окрестности a снизу часто встречаются точки из s.

LaTeX

$$frequently_nhds_mem$$

Lean4

theorem frequently_nhds_mem {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : ∃ᶠ x in 𝓝 a, x ∈ s :=
  (ha.frequently_mem hs).filter_mono inf_le_left

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