English
In a Conditionally Complete Linear Order with a compatible topology and first-countability, for any nonempty S that is bounded above, there exists a sequence (u_n) of elements of α which is monotone and converges to sSup S, with each u_n ∈ S.
Русский
Пусть S — ненулевое множество, ограниченное сверху, в условно полно упорядоченном множестве α с топологией. Тогда существует монотонная последовательность элементов S, сходящаяся к sSup S.
LaTeX
$$$$\exists u: \mathbb{N} \to \alpha,\; \text{Monotone}(u) \wedge \operatorname{Tendsto} u\ atTop\ (\mathcal{N}(\operatorname{sSup} S)) \wedge \forall n\, u_n \in S.$$$$
Lean4
theorem exists_seq_tendsto_sSup {α : Type*} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α]
[FirstCountableTopology α] {S : Set α} (hS : S.Nonempty) (hS' : BddAbove S) :
∃ u : ℕ → α, Monotone u ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ n, u n ∈ S :=
by
rcases (isLUB_csSup hS hS').exists_seq_monotone_tendsto hS with ⟨u, hu⟩
exact ⟨u, hu.1, hu.2.2⟩
