English
Let t ⊆ α with x as a greatest lower bound and t nonempty. Then there exists an antitone (nonincreasing) sequence u_n in α with u_n ∈ t for all n, x ≤ u_n for all n, and u_n → x.
Русский
Для множества t, чьим наибольшим нижним пределом является x, существует антипод последовательности в t, сходящейся к x.
LaTeX
$$$$\exists u: \mathbb{N} \to \alpha,\; \text{Antitone}(u) \wedge (\forall n, x \le u_n) \wedge \operatorname{Tendsto} u\ atTop\ (\mathcal{N} x) \wedge \forall n, u_n \in t.$$$$
Lean4
theorem exists_seq_antitone_tendsto {t : Set α} {x : α} [IsCountablyGenerated (𝓝 x)] (htx : IsGLB t x)
(ht : t.Nonempty) : ∃ u : ℕ → α, Antitone u ∧ (∀ n, x ≤ u n) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ n, u n ∈ t :=
IsLUB.exists_seq_monotone_tendsto (α := αᵒᵈ) htx ht
