English
Lebesgue number lemma in the nhds' form: given a compact K and a family, there is a uniform neighborhood V such that for each x ∈ K there exists y ∈ K with ball x V subset of U(y,y.2).
Русский
Лемма Лебега в форме nhds': дано компактное K и семейство, существует V из равномерности так, что для каждого x ∈ K найдется y ∈ K с ball x V ⊆ U(y,y.2).
LaTeX
$$$ {U : (x : α) → x \in K → Set α} (hK : IsCompact K) (hU : ∀ x hx, U x hx ∈ 𝓝 x) : \exists V ∈ 𝓤 α, ∀ x ∈ K, ∃ y : K, ball x V ⊆ U y y.2$$$
Lean4
theorem lebesgue_number_lemma_nhds' {U : (x : α) → x ∈ K → Set α} (hK : IsCompact K) (hU : ∀ x hx, U x hx ∈ 𝓝 x) :
∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ y : K, ball x V ⊆ U y y.2 :=
by
rcases
lebesgue_number_lemma (U := fun x : K => interior (U x x.2)) hK (fun _ => isOpen_interior)
(fun x hx => mem_iUnion.2 ⟨⟨x, hx⟩, mem_interior_iff_mem_nhds.2 (hU x hx)⟩) with
⟨V, V_uni, hV⟩
exact ⟨V, V_uni, fun x hx => (hV x hx).imp fun _ hy => hy.trans interior_subset⟩
