English
If a is the least upper bound of a nonempty set s and α is ordered, then there are frequently points of s arbitrarily close to a from below.
Русский
Пусть a есть наименьшее верхнее предел множества s и существует не пустое s; тогда рядом с a снизу часто встречаются точки из s.
LaTeX
$$frequently_mem$$
Lean4
theorem frequently_mem {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : ∃ᶠ x in 𝓝[≤] a, x ∈ s :=
by
rcases hs with ⟨a', ha'⟩
intro h
rcases (ha.1 ha').eq_or_lt with (rfl | ha'a)
· exact h.self_of_nhdsWithin le_rfl ha'
· rcases (mem_nhdsLE_iff_exists_Ioc_subset' ha'a).1 h with ⟨b, hba, hb⟩
rcases ha.exists_between hba with ⟨b', hb's, hb'⟩
exact hb hb' hb's
