Uniform separation of compact and closed set

Stream: Is there code for X?

[Anatole Dedecker]

Do we have the following?

import topology.uniform_space.basic

open uniform_space
open_locale uniformity

lemma bourbaki_GT_II_4_prop4 {X : Type*} [uniform_space X] {A B : set X}
  (hA : is_compact A) (hB : is_closed B) (h : disjoint A B) :
  ∃ V ∈ 𝓤 X, (⋃ x ∈ A, ball x V) ∩ (⋃ x ∈ B, ball x V) = ∅ :=
sorry

(and btw, do we have a better way to express ⋃ x ∈ A, ball x V? Like docs#metric.thickening but for any entourage)

[Anatole Dedecker]

(The reference is for the French edition of Bourbaki, I hope it's enough clues to find it in the English version)

[Anatole Dedecker]

Ok so it follows quite easily from Yury's docs#is_compact.nhds_set_basis_uniformity, which is funny because Bourbaki does it the other way around.

import topology.uniform_space.basic

open uniform_space set
open_locale uniformity filter topological_space

lemma bourbaki_GT_II_4_prop4 {X : Type*} [uniform_space X] {A B : set X}
  (hA : is_compact A) (hB : is_closed B) (h : disjoint A B) :
  ∃ V ∈ 𝓤 X, disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V) :=
begin
  have : Bᶜ ∈ 𝓝ˢ A := hB.is_open_compl.mem_nhds_set.mpr h.le_compl_right,
  rw (hA.nhds_set_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, λ x, _⟩,
  simp only [inf_eq_inter, mem_inter_iff, mem_Union₂],
  rintro ⟨⟨a, ha, hxa⟩, ⟨b, hb, hxb⟩⟩,
  rw mem_ball_symmetry hVsymm at hxa hxb,
  exact hUAB (mem_Union₂_of_mem ha $ hVU $ mem_comp_of_mem_ball hVsymm hxa hxb) hb
end

[Anatole Dedecker]

If someone wants to try the other way to see if it's shorter that would probably be fun, but that's good enough for me

[Anatole Dedecker]

#16747