English
If y < x in a densely ordered, first-countable, order-topology line, there exists a strictly increasing sequence u with u(n) ∈ (y,x) and u(n) → x.
Русский
Если y < x в плотно упорядоченном, первая счетная топология, существует строго возрастающая последовательность u с u(n) ∈ (y,x) и u(n) → x.
LaTeX
$$hy : y < x → ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n ∈ Ioo y x) ∧ Tendsto u atTop (nhds x)$$
Lean4
theorem exists_seq_strictMono_tendsto' {α : Type*} [LinearOrder α] [TopologicalSpace α] [DenselyOrdered α]
[OrderTopology α] [FirstCountableTopology α] {x y : α} (hy : y < x) :
∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x) :=
by
have hx : x ∉ Ioo y x := fun h => (lt_irrefl x h.2).elim
have ht : Set.Nonempty (Ioo y x) := nonempty_Ioo.2 hy
rcases (isLUB_Ioo hy).exists_seq_strictMono_tendsto_of_notMem hx ht with ⟨u, hu⟩
exact ⟨u, hu.1, hu.2.2.symm⟩
