English
On the real line, Tendsto holds for the mapping y ↦ Icc(y, x) as y approaches x from above and from below, with respect to the Vitali filter at x.
Русский
На вещественной линии при устремлении y к x слева и справа относительно фильтра Витали выполняется предел для Icc(y,x).
LaTeX
$$$\ Tendsto\bigl( y \mapsto Icc(y,x) \bigr)\; (\text{предел в } \mathcal{N}_{x})$$$
Lean4
theorem tendsto_Icc_vitaliFamily_right (x : ℝ) :
Tendsto (fun y => Icc x y) (𝓝[>] x) ((vitaliFamily (volume : Measure ℝ) 1).filterAt x) :=
by
refine (VitaliFamily.tendsto_filterAt_iff _).2 ⟨?_, ?_⟩
· filter_upwards [self_mem_nhdsWithin] with y hy using Icc_mem_vitaliFamily_at_right hy
· intro ε εpos
filter_upwards [Icc_mem_nhdsGT <| show x < x + ε by linarith] with y hy
rw [closedBall_eq_Icc]
exact Icc_subset_Icc (by linarith) hy.2
