English
Definition of Vitali covering family: a structured way to select a disjoint subfamily with controlled enlargement to cover the original family.
Русский
Определение семейства покрытий Витали: выверенный способ выбрать непересекающееся подмножество с контролируемым увеличением, чтобы покрыть исходную семью.
LaTeX
$$$\text{VitaliFamily } μ := \text{структура с setsAt, filterAt и др.}$$$
Lean4
theorem tendsto_Icc_vitaliFamily_left (x : ℝ) :
Tendsto (fun y => Icc y x) (𝓝[<] 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_left hy
· intro ε εpos
filter_upwards [Icc_mem_nhdsLT <| show x - ε < x by linarith] with y hy
rw [closedBall_eq_Icc]
exact Icc_subset_Icc hy.1 (by linarith)
