English
Under the same hypotheses as before, there exists a strictly increasing sequence (u_n) with u_n < x for all n and such that u_n converges to x in the left-hand neighborhood, i.e., Tendsto u to 𝓝[<] x.
Русский
При тех же условиях существует последовательность, строго возрастающая и лежащая слева от x, сходящаяся к x внутри левой окрестности.
LaTeX
$$$$\exists u: \mathbb{N} \to \alpha,\; \text{StrictMono}(u) \wedge (\forall n\, u_n < x) \wedge \operatorname{Tendsto}(u)\ atTop\ (\mathcal{N}_{[<]} x).$$$$
Lean4
theorem exists_seq_strictMono_tendsto_nhdsWithin [DenselyOrdered α] [NoMinOrder α] [FirstCountableTopology α] (x : α) :
∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n < x) ∧ Tendsto u atTop (𝓝[<] x) :=
let ⟨u, hu, hx, h⟩ := exists_seq_strictMono_tendsto x
⟨u, hu, hx, tendsto_nhdsWithin_mono_right (range_subset_iff.2 hx) <| tendsto_nhdsWithin_range.2 h⟩
