exists_uniform_thickening_of_basis

English

If K is compact and {V_i} is a basis of entourages, then the family {⋃_{x∈K} ball(x,V_i)} forms a basis for nhdsˢ K.

Русский

Если K компактно и {V_i} базис окружностей, то {⋃_{x∈K} ball(x,V_i)} образуют базис для nhdsˢ K.

LaTeX

$$$$ (\\mathcal{N}^\\# K).HasBasis p (\\lambda i. \\bigcup_{x \\in K} \\mathrm{ball}(x,V_i)) $$$$

Lean4

theorem exists_uniform_thickening_of_basis {p : ι → Prop} {s : ι → Set (α × α)} (hU : (𝓤 α).HasBasis p s) {A B : Set α}
    (hA : IsCompact A) (hB : IsClosed B) (h : Disjoint A B) :
    ∃ i, p i ∧ Disjoint (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i)) :=
  by
  rcases h.exists_uniform_thickening hA hB with ⟨V, hV, hVAB⟩
  rcases hU.mem_iff.1 hV with ⟨i, hi, hiV⟩
  exact ⟨i, hi, hVAB.mono (iUnion₂_mono fun a _ => ball_mono hiV a) (iUnion₂_mono fun b _ => ball_mono hiV b)⟩

Похожие утверждения