English
There exists a monotone sequence J: ℕ → Box ι such that for all n, Box.Icc(J(n)) ⊆ Box.Ioo I, and the lower and upper bounds converge to I.lower and I.upper respectively.
Русский
Существует монотонная последовательность J: ℕ → Box ι такая, что для всех n выполняется Box.Icc(J(n)) ⊆ Box.Ioo I, и границы снизу и сверху сходятся к I.lower и I.upper соответственно.
LaTeX
$$$$ \\exists J:\\mathbb{N} \\to_o Box\\ ι,\\; (\\forall n, Box.Icc (J(n)) \\subseteq Box.Ioo I) \\land Tendsto (lower \\circ J) atTop (\\nhds I.lower) \\land Tendsto (upper \\circ J) atTop (\\nhds I.upper) $$$$
Lean4
theorem exists_seq_mono_tendsto (I : Box ι) :
∃ J : ℕ →o Box ι,
(∀ n, Box.Icc (J n) ⊆ Box.Ioo I) ∧
Tendsto (lower ∘ J) atTop (𝓝 I.lower) ∧ Tendsto (upper ∘ J) atTop (𝓝 I.upper) :=
by
choose a b ha_anti hb_mono ha_mem hb_mem hab ha_tendsto hb_tendsto using fun i ↦
exists_seq_strictAnti_strictMono_tendsto (I.lower_lt_upper i)
exact
⟨⟨fun k ↦ ⟨flip a k, flip b k, fun i ↦ hab _ _ _⟩, fun k l hkl ↦
le_iff_bounds.2 ⟨fun i ↦ (ha_anti i).antitone hkl, fun i ↦ (hb_mono i).monotone hkl⟩⟩,
fun n x hx i _ ↦ ⟨(ha_mem _ _).1.trans_le (hx.1 _), (hx.2 _).trans_lt (hb_mem _ _).2⟩,
tendsto_pi_nhds.2 ha_tendsto, tendsto_pi_nhds.2 hb_tendsto⟩
