English
Let a compact set K be covered by open sets U_i. There exists a radius V such that every point in K has a ball of radius V contained in some U_i.
Русский
Пусть компактное множество K покрывается открытыми множествами U_i. Существует радиус V, такой что любая точка x∈K имеет шар радиуса V, который полностью лежит в каком-либо U_i.
LaTeX
$$$\exists V \in \mathcal{U}(\alpha) \;\forall x \in K, \exists i, B(x,V) \subseteq U_i$$$
Lean4
/-- Let `c : ι → Set α` be an open cover of a compact set `s`. Then there exists an entourage
`n` such that for each `x ∈ s` its `n`-neighborhood is contained in some `c i`. -/
theorem lebesgue_number_lemma {ι : Sort*} {U : ι → Set α} (hK : IsCompact K) (hopen : ∀ i, IsOpen (U i))
(hcover : K ⊆ ⋃ i, U i) : ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ i, ball x V ⊆ U i :=
by
have : ∀ x ∈ K, ∃ i, ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i := fun x hx ↦
by
obtain ⟨i, hi⟩ := mem_iUnion.1 (hcover hx)
rw [← (hopen i).mem_nhds_iff, nhds_eq_comap_uniformity, ← lift'_comp_uniformity] at hi
exact ⟨i, (((basis_sets _).lift' <| monotone_id.compRel monotone_id).comap _).mem_iff.1 hi⟩
choose ind W hW hWU using this
rcases hK.elim_nhds_subcover' (fun x hx ↦ ball x (W x hx)) (fun x hx ↦ ball_mem_nhds _ (hW x hx)) with ⟨t, ht⟩
refine ⟨⋂ x ∈ t, W x x.2, (biInter_finset_mem _).2 fun x _ ↦ hW x x.2, fun x hx ↦ ?_⟩
rcases mem_iUnion₂.1 (ht hx) with ⟨y, hyt, hxy⟩
exact ⟨ind y y.2, fun z hz ↦ hWU _ _ ⟨x, hxy, mem_iInter₂.1 hz _ hyt⟩⟩
