English
The function c.lim is continuous as a map from X to ℝ.
Русский
Функция c.lim непрерывна как отображение из X в ℝ.
LaTeX
$$$ \text{Continuous}(c.lim) $$$
Lean4
/-- Continuity of `Urysohns.CU.lim`. See module docstring for a sketch of the proofs. -/
theorem continuous_lim (c : CU P) : Continuous c.lim :=
by
obtain ⟨h0, h1234, h1⟩ : 0 < (2⁻¹ : ℝ) ∧ (2⁻¹ : ℝ) < 3 / 4 ∧ (3 / 4 : ℝ) < 1 := by norm_num
refine
continuous_iff_continuousAt.2 fun x =>
(Metric.nhds_basis_closedBall_pow (h0.trans h1234) h1).tendsto_right_iff.2 fun n _ => ?_
simp only [Metric.mem_closedBall]
induction n generalizing c with
| zero =>
filter_upwards with y
rw [pow_zero]
exact Real.dist_le_of_mem_Icc_01 (c.lim_mem_Icc _) (c.lim_mem_Icc _)
| succ n ihn =>
by_cases hxl : x ∈ c.left.U
· filter_upwards [IsOpen.mem_nhds c.left.open_U hxl, ihn c.left] with _ hyl hyd
rw [pow_succ', c.lim_eq_midpoint, c.lim_eq_midpoint, c.right.lim_of_mem_C _ (c.left_U_subset_right_C hyl),
c.right.lim_of_mem_C _ (c.left_U_subset_right_C hxl)]
refine (dist_midpoint_midpoint_le _ _ _ _).trans ?_
rw [dist_self, add_zero, div_eq_inv_mul]
gcongr
· replace hxl : x ∈ c.left.right.Cᶜ := compl_subset_compl.2 c.left.right.subset hxl
filter_upwards [IsOpen.mem_nhds (isOpen_compl_iff.2 c.left.right.closed_C) hxl, ihn c.left.right,
ihn c.right] with y hyl hydl hydr
replace hxl : x ∉ c.left.left.U := compl_subset_compl.2 c.left.left_U_subset_right_C hxl
replace hyl : y ∉ c.left.left.U := compl_subset_compl.2 c.left.left_U_subset_right_C hyl
simp only [pow_succ, c.lim_eq_midpoint, c.left.lim_eq_midpoint, c.left.left.lim_of_notMem_U _ hxl,
c.left.left.lim_of_notMem_U _ hyl]
refine (dist_midpoint_midpoint_le _ _ _ _).trans ?_
refine (div_le_div_of_nonneg_right (add_le_add_right (dist_midpoint_midpoint_le _ _ _ _) _) zero_le_two).trans ?_
rw [dist_self, zero_add]
set r := (3 / 4 : ℝ) ^ n
calc
_ ≤ (r / 2 + r) / 2 := by gcongr
_ = _ := by field_simp; ring
