English
If IsLUB t x holds and x ∉ t and t nonempty, there exists a strictly increasing sequence u with u(n) ∈ t and u(n) → x along atTop.
Русский
Если IsLUB t x и x ∉ t и t непусто, существует строго возрастающая последовательность u с u(n) ∈ t и u(n) → x при atTop.
LaTeX
$$htx : IsLUB t x → notMem : x ∉ t → ht : t.Nonempty → ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n ∈ t) ∧ Tendsto u atTop (nhds x)$$
Lean4
theorem exists_seq_monotone_tendsto {t : Set α} {x : α} [IsCountablyGenerated (𝓝 x)] (htx : IsLUB t x)
(ht : t.Nonempty) : ∃ u : ℕ → α, Monotone u ∧ (∀ n, u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ n, u n ∈ t :=
by
by_cases h : x ∈ t
· exact ⟨fun _ => x, monotone_const, fun n => le_rfl, tendsto_const_nhds, fun _ => h⟩
· rcases htx.exists_seq_strictMono_tendsto_of_notMem h ht with ⟨u, hu⟩
exact ⟨u, hu.1.monotone, fun n => (hu.2.1 n).le, hu.2.2⟩
