frequently_mem

Mathlib.Topology.Order.IsLUB

URI: https://scilib.ai/kg/mathlib#IsGLB.frequently_mem

English

For IsLUB, there are frequently points of s near a in the nhds within a.

Русский

Для IsLUB существуют часто встречающиеся точки множества s рядом с a в окрестности a.

LaTeX

$$frequently_mem$$

Lean4

theorem frequently_mem {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) : ∃ᶠ x in 𝓝[≥] a, x ∈ s :=
  IsLUB.frequently_mem (α := αᵒᵈ) ha hs

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru