English
If index-valued boxes J_n converge in lower and upper bounds to I, then the union over n of Ioo(J_n) equals Ioo(I).
Русский
Если набор коробок J_n сходится по нижним и верхним границам к I, то объединение Ioo(J_n) по всем n равно Ioo(I).
LaTeX
$$$\bigcup_{n} Box.Ioo (J n) = Box.Ioo I$ (under appropriate Tendsto hypotheses).$$
Lean4
theorem iUnion_Ioo_of_tendsto [Finite ι] {I : Box ι} {J : ℕ → Box ι} (hJ : Monotone J)
(hl : Tendsto (lower ∘ J) atTop (𝓝 I.lower)) (hu : Tendsto (upper ∘ J) atTop (𝓝 I.upper)) :
⋃ n, Box.Ioo (J n) = Box.Ioo I :=
have hl' : ∀ i, Antitone fun n ↦ (J n).lower i := fun i ↦
(monotone_eval i).comp_antitone (antitone_lower.comp_monotone hJ)
have hu' : ∀ i, Monotone fun n ↦ (J n).upper i := fun i ↦ (monotone_eval i).comp (monotone_upper.comp hJ)
calc
⋃ n, Box.Ioo (J n) = pi univ fun i ↦ ⋃ n, Ioo ((J n).lower i) ((J n).upper i) :=
iUnion_univ_pi_of_monotone fun i ↦ (hl' i).Ioo (hu' i)
_ = Box.Ioo I :=
pi_congr rfl fun i _ ↦
iUnion_Ioo_of_mono_of_isGLB_of_isLUB (hl' i) (hu' i) (isGLB_of_tendsto_atTop (hl' i) (tendsto_pi_nhds.1 hl _))
(isLUB_of_tendsto_atTop (hu' i) (tendsto_pi_nhds.1 hu _))
