English
Let t ⊆ α have x as a greatest lower bound, with x ∉ t and t nonempty. Then there exists a sequence u: ℕ → α that is strictly decreasing (StrictAnti), lies above x (x < u_n for all n), tends to x, and all u_n belong to t.
Русский
Пусть t имеет наибольшую нижнюю грань x и x не принадлежит t; тогда существует строго убывающая последовательность из t, которая сходится к x и лежит в t.
LaTeX
$$$$\exists u: \mathbb{N} \to \alpha,\; \text{StrictAnti}(u) \wedge (\forall n, x < u_n) \wedge \operatorname{Tendsto} u\ atTop\ (\mathcal{N} x) \wedge \forall n, u_n \in t.$$$$
Lean4
theorem exists_seq_strictAnti_tendsto_of_notMem {t : Set α} {x : α} [IsCountablyGenerated (𝓝 x)] (htx : IsGLB t x)
(notMem : x ∉ t) (ht : t.Nonempty) :
∃ u : ℕ → α, StrictAnti u ∧ (∀ n, x < u n) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ n, u n ∈ t :=
IsLUB.exists_seq_strictMono_tendsto_of_notMem (α := αᵒᵈ) htx notMem ht
