English
Let s be dense in α. For any x ∈ α there exists a strictly increasing sequence (u_n) with u_n ∈ Iio x ∩ s for all n, and u_n → x.
Русский
Плотное подмножество s в α: существует строгая монотонная последовательность, каждая её точка меньше x, и она сходится к x.
LaTeX
$$$$\exists u: \mathbb{N} \to \alpha,\; \text{StrictMono}(u) \wedge (\forall n\, u_n \in (Iio x \cap s)) \wedge \operatorname{Tendsto} u\ atTop\ (\mathcal{N} x).$$$$
Lean4
theorem exists_seq_strictMono_tendsto [DenselyOrdered α] [NoMinOrder α] [FirstCountableTopology α] {s : Set α}
(hs : Dense s) (x : α) : ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n ∈ (Iio x ∩ s)) ∧ Tendsto u atTop (𝓝 x) :=
by
obtain ⟨y, hy⟩ := exists_lt x
apply hs.exists_seq_strictMono_tendsto_of_lt (exists_lt x).choose_spec |>.imp
simp_all
