English
Let f: β → α with dense range, α densely ordered. For nonempty S ⊆ α that is bounded above, there exists a sequence u: ℕ → α with u_n ∈ S, monotone, and Tendsto to sSup S.
Русский
Пусть S ненулево и ограничено сверху в условно полно упорядоченном множестве α. Тогда существует монотонная последовательность элементов S, сходящаяся к супремуму S.
LaTeX
$$$$\exists u: \mathbb{N} \to \alpha,\; \text{Monotone}(u) \wedge \operatorname{Tendsto} u\ atTop\ (\mathcal{N}(\operatorname{sSup} S)) \wedge \forall n\, u_n \in S.$$$$
Lean4
theorem exists_seq_strictMono_tendsto {β : Type*} [LinearOrder β] [DenselyOrdered α] [NoMinOrder α]
[FirstCountableTopology α] {f : β → α} (hf : DenseRange f) (hmono : Monotone f) (x : α) :
∃ u : ℕ → β, StrictMono u ∧ (∀ n, f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x) :=
by
rcases Dense.exists_seq_strictMono_tendsto hf x with ⟨u, hu, huxf, hlim⟩
have hux (n : ℕ) : u n ∈ Iio x := (huxf n).1
have huf (n : ℕ) : u n ∈ range f := (huxf 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, hux, hlim⟩
