English
If IsLUB t x holds and x ∉ t and t is nonempty, there exists a sequence u: N → α that is strictly increasing, with u(n) < x for all n, tends to x along atTop, and with u(n) ∈ t for all n.
Русский
Если IsLUB t x и x не принадлежит t, и t непусто, существует последовательность u: N → α строго возрастающая, такая что u(n) < x, u(n) → x сверху, и каждый u(n) ∈ t.
LaTeX
$$htx : IsLUB t x → notMem : x ∉ t → ht : t.Nonempty → ∃ u:ℕ→α, StrictMono u ∧ (∀ n, u n < x) ∧ Tendsto u atTop (nhds x) ∧ ∀ n, u n ∈ t$$
Lean4
theorem exists_seq_strictMono_tendsto_of_notMem {t : Set α} {x : α} [IsCountablyGenerated (𝓝 x)] (htx : IsLUB t x)
(notMem : x ∉ t) (ht : t.Nonempty) :
∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ n, u n ∈ t :=
by
obtain ⟨v, hvx, hvt⟩ := exists_seq_forall_of_frequently (htx.frequently_mem ht)
replace hvx := hvx.mono_right nhdsWithin_le_nhds
have hvx' : ∀ {n}, v n < x := (htx.1 (hvt _)).lt_of_ne (ne_of_mem_of_not_mem (hvt _) notMem)
have : ∀ k, ∀ᶠ l in atTop, v k < v l := fun k => hvx.eventually (lt_mem_nhds hvx')
choose N hN hvN using fun k => ((eventually_gt_atTop k).and (this k)).exists
refine
⟨fun k => v (N^[k] 0), strictMono_nat_of_lt_succ fun _ => ?_, fun _ => hvx',
hvx.comp (strictMono_nat_of_lt_succ fun _ => ?_).tendsto_atTop, fun _ => hvt _⟩
· rw [iterate_succ_apply']; exact hvN _
· rw [iterate_succ_apply']; exact hN _
