English
Let c be an element of Urysohns.CU. Then the limiting value at x is the real midpoint of the left and right limiting values: c.lim x = midpoint(ℝ, c.left.lim x, c.right.lim x).
Русский
Пусть c принадлежит Urysohns.CU. Тогда предел c.lim x равен арифметической средине левой и правой ограничений: c.lim x = midpoint(ℝ)(c.left.lim x)(c.right.lim x).
LaTeX
$$$ c.lim x = \operatorname{midpoint} \mathbb{R} (c.left.lim x) (c.right.lim x) $$$
Lean4
theorem lim_eq_midpoint (c : CU P) (x : X) : c.lim x = midpoint ℝ (c.left.lim x) (c.right.lim x) :=
by
refine tendsto_nhds_unique (c.tendsto_approx_atTop x) ((tendsto_add_atTop_iff_nat 1).1 ?_)
simp only [approx]
exact (c.left.tendsto_approx_atTop x).midpoint (c.right.tendsto_approx_atTop x)
