English
Let α be densely ordered, with no minimum element and a first-countable topology. For every x ∈ α there exists a strictly increasing sequence (u_n) in α such that u_n < x for all n and u_n tends to x as n → ∞.
Русский
Пусть α — плотно упорядоченный набор с топологией первого счёта и без минимального элемента. Для любого x ∈ α существует строго возрастающая последовательность u_n ∈ α такая, что u_n < x для всех n и u_n сходится к x.
LaTeX
$$$$\exists u: \mathbb{N} \to \alpha,\; \text{StrictMono}(u) \wedge (\forall n\, u_n < x) \wedge \lim_{n\to\infty} u_n = x.$$$$
Lean4
theorem exists_seq_strictMono_tendsto [DenselyOrdered α] [NoMinOrder α] [FirstCountableTopology α] (x : α) :
∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n < x) ∧ Tendsto u atTop (𝓝 x) :=
by
obtain ⟨y, hy⟩ : ∃ y, y < x := exists_lt x
rcases exists_seq_strictMono_tendsto' hy with ⟨u, hu_mono, hu_mem, hux⟩
exact ⟨u, hu_mono, fun n => (hu_mem n).2, hux⟩
