English
A symmetric version: the same basis description holds with a symmetric treatment of pairs in the product space.
Русский
Симметричная версия: то же самое основание выполняется с симметричным рассмотрением пар в произведении пространств.
LaTeX
$$$$ (\\mathcal{N}^\\# K).HasBasis p (V_i)$$ where each V_i is understood symmetrically on pairs.$$
Lean4
theorem exists_uniform_thickening {A B : Set α} (hA : IsCompact A) (hB : IsClosed B) (h : Disjoint A B) :
∃ V ∈ 𝓤 α, Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V) :=
by
have : Bᶜ ∈ 𝓝ˢ A := hB.isOpen_compl.mem_nhdsSet.mpr h.le_compl_right
rw [(hA.nhdsSet_basis_uniformity (Filter.basis_sets _)).mem_iff] at this
rcases this with ⟨U, hU, hUAB⟩
rcases comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVsymm, hVU⟩
refine ⟨V, hV, Set.disjoint_left.mpr fun x => ?_⟩
simp only [mem_iUnion₂]
rintro ⟨a, ha, hxa⟩ ⟨b, hb, hxb⟩
rw [mem_ball_symmetry hVsymm] at hxa hxb
exact hUAB (mem_iUnion₂_of_mem ha <| hVU <| mem_comp_of_mem_ball hVsymm hxa hxb) hb
