English
Let f: β → α have dense range, α densely ordered. If y < x, there exists u: ℕ → β with u strictly monotone, f(u_n) ∈ Ioo(y, x) for all n, and f∘u tends to x.
Русский
Если отображение имеет плотный образ и упорядочено линейно, то при y < x существует монотонная последовательность в домене, чьи образы лежат в Ioo(y, x) и сходятся к x.
LaTeX
$$$$\exists u: \mathbb{N} \to \beta,\; \text{StrictMono}(u) \wedge (\forall n, f(u_n) \in Ioo(y,x)) \\wedge \operatorname{Tendsto}(f \circ u)\ atTop\ (\mathcal{N} x).$$$$
Lean4
theorem exists_seq_strictMono_tendsto_of_lt {β : Type*} [LinearOrder β] [DenselyOrdered α] [FirstCountableTopology α]
{f : β → α} {x y : α} (hf : DenseRange f) (hmono : Monotone f) (hlt : y < x) :
∃ u : ℕ → β, StrictMono u ∧ (∀ n, f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x) :=
by
rcases Dense.exists_seq_strictMono_tendsto_of_lt hf hlt with ⟨u, hu, huyxf, hlim⟩
have huyx (n : ℕ) : u n ∈ Ioo y x := (huyxf n).1
have huf (n : ℕ) : u n ∈ range f := (huyxf n).2
choose v hv using huf
obtain rfl : f ∘ v = u := funext hv
exact ⟨v, fun a b hlt ↦ hmono.reflect_lt <| hu hlt, huyx, hlim⟩
