feat(topology/uniform_space/compact_separated): drop unneeded assumpt…

…ions (#16457)

Lemmas in this file don't need `[separated_space _]` / `is_separated _` assumption. Also add `nhds_set` versions of some lemmas.

src/topology/algebra/uniform_group.lean

@@ -379,14 +379,14 @@ variables (G : Type*) [group G] [topological_space G] [topological_group G]
 
 Warning: in general the right and left uniformities do not coincide and so one does not obtain a
 `uniform_group` structure. Two important special cases where they _do_ coincide are for
-commutative groups (see `topological_comm_group_is_uniform`) and for compact Hausdorff groups (see
+commutative groups (see `topological_comm_group_is_uniform`) and for compact groups (see
 `topological_group_is_uniform_of_compact_space`). -/
 @[to_additive "The right uniformity on a topological additive group (as opposed to the left
 uniformity).
 
 Warning: in general the right and left uniformities do not coincide and so one does not obtain a
 `uniform_add_group` structure. Two important special cases where they _do_ coincide are for
-commutative additive groups (see `topological_add_comm_group_is_uniform`) and for compact Hausdorff
+commutative additive groups (see `topological_add_comm_group_is_uniform`) and for compact
 additive groups (see `topological_add_comm_group_is_uniform_of_compact_space`)."]
 def topological_group.to_uniform_space : uniform_space G :=
 { uniformity          := comap (λp:G×G, p.2 / p.1) (𝓝 1),
@@ -440,9 +440,8 @@ local attribute [instance] topological_group.to_uniform_space
   𝓤 G = comap (λp:G×G, p.2 / p.1) (𝓝 (1 : G)) := rfl
 
 @[to_additive] lemma topological_group_is_uniform_of_compact_space
-  [compact_space G] [t2_space G] : uniform_group G :=
+  [compact_space G] : uniform_group G :=
 ⟨begin
-  haveI : separated_space G := separated_iff_t2.mpr (by apply_instance),
   apply compact_space.uniform_continuous_of_continuous,
   exact continuous_div',
 end⟩

src/topology/nhds_set.lean

@@ -35,6 +35,9 @@ Sup (nhds '' s)
 
 localized "notation (name := nhds_set) `𝓝ˢ` := nhds_set" in topological_space
 
+lemma nhds_set_diagonal (α) [topological_space (α × α)] : 𝓝ˢ (diagonal α) = ⨆ x, 𝓝 (x, x) :=
+by { rw [nhds_set, ← range_diag, ← range_comp], refl }
+
 lemma mem_nhds_set_iff_forall : s ∈ 𝓝ˢ t ↔ ∀ (x : α), x ∈ t → s ∈ 𝓝 x :=
 by simp_rw [nhds_set, filter.mem_Sup, ball_image_iff]
 

src/topology/subset_properties.lean

@@ -803,6 +803,9 @@ lemma is_compact_range [compact_space α] {f : α → β} (hf : continuous f) :
   is_compact (range f) :=
 by rw ← image_univ; exact compact_univ.image hf
 
+lemma is_compact_diagonal [compact_space α] : is_compact (diagonal α) :=
+@range_diag α ▸ is_compact_range (continuous_id.prod_mk continuous_id)
+
 /-- If X is is_compact then pr₂ : X × Y → Y is a closed map -/
 theorem is_closed_proj_of_is_compact
   {X : Type*} [topological_space X] [compact_space X]

src/topology/uniform_space/basic.lean

@@ -5,6 +5,8 @@ Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
 -/
 import order.filter.small_sets
 import topology.subset_properties
+import topology.nhds_set
+
 /-!
 # Uniform spaces
 
@@ -681,6 +683,32 @@ lemma mem_nhds_right (y : α) {s : set (α×α)} (h : s ∈ 𝓤 α) :
   {x : α | (x, y) ∈ s} ∈ 𝓝 y :=
 mem_nhds_left _ (symm_le_uniformity h)
 
+lemma is_compact.nhds_set_basis_uniformity {p : ι → Prop} {s : ι → set (α × α)}
+  (hU : (𝓤 α).has_basis p s) {K : set α} (hK : is_compact K) :
+  (𝓝ˢ K).has_basis p (λ i, ⋃ x ∈ K, ball x (s i)) :=
+begin
+  refine ⟨λ U, _⟩,
+  simp only [mem_nhds_set_iff_forall, (nhds_basis_uniformity' hU).mem_iff, Union₂_subset_iff],
+  refine ⟨λ H, _, λ ⟨i, hpi, hi⟩ x hx, ⟨i, hpi, hi x hx⟩⟩,
+  replace H : ∀ x ∈ K, ∃ i : {i // p i}, ball x (s i ○ s i) ⊆ U,
+  { intros x hx,
+    rcases H x hx with ⟨i, hpi, hi⟩,
+    rcases comp_mem_uniformity_sets (hU.mem_of_mem hpi) with ⟨t, ht_mem, ht⟩,
+    rcases hU.mem_iff.1 ht_mem with ⟨j, hpj, hj⟩,
+    exact ⟨⟨j, hpj⟩, subset.trans (ball_mono ((comp_rel_mono hj hj).trans ht) _) hi⟩ },
+  haveI : nonempty {a // p a}, from nonempty_subtype.2 hU.ex_mem,
+  choose! I hI using H,
+  rcases hK.elim_nhds_subcover (λ x, ball x $ s (I x))
+    (λ x hx, ball_mem_nhds _ $ hU.mem_of_mem (I x).2) with ⟨t, htK, ht⟩,
+  obtain ⟨i, hpi, hi⟩ : ∃ i (hpi : p i), s i ⊆ ⋂ x ∈ t, s (I x),
+    from hU.mem_iff.1 ((bInter_finset_mem t).2 (λ x hx, hU.mem_of_mem (I x).2)),
+  rw [subset_Inter₂_iff] at hi,
+  refine ⟨i, hpi, λ x hx, _⟩,
+  rcases mem_Union₂.1 (ht hx) with ⟨z, hzt : z ∈ t, hzx : x ∈ ball z (s (I z))⟩,
+  calc ball x (s i) ⊆ ball z (s (I z) ○ s (I z)) : λ y hy, ⟨x, hzx, hi z hzt hy⟩
+                ... ⊆ U                          : hI z (htK z hzt),
+end
+
 lemma tendsto_right_nhds_uniformity {a : α} : tendsto (λa', (a', a)) (𝓝 a) (𝓤 α) :=
 assume s, mem_nhds_right a
 
@@ -764,6 +792,10 @@ end
 lemma supr_nhds_le_uniformity : (⨆ x : α, 𝓝 (x, x)) ≤ 𝓤 α :=
 supr_le nhds_le_uniformity
 
+/-- Entourages are neighborhoods of the diagonal. -/
+lemma nhds_set_diagonal_le_uniformity : 𝓝ˢ (diagonal α) ≤ 𝓤 α :=
+(nhds_set_diagonal α).trans_le supr_nhds_le_uniformity
+
 /-!
 ### Closure and interior in uniform spaces
 -/
@@ -1355,25 +1387,22 @@ theorem uniformity_prod [uniform_space α] [uniform_space β] : 𝓤 (α × β)
   (𝓤 β).comap (λp:(α × β) × α × β, (p.1.2, p.2.2)) :=
 rfl
 
+lemma uniformity_prod_eq_comap_prod [uniform_space α] [uniform_space β] :
+  𝓤 (α × β) = comap (λ p : (α × β) × (α × β), ((p.1.1, p.2.1), (p.1.2, p.2.2))) (𝓤 α ×ᶠ 𝓤 β) :=
+by rw [uniformity_prod, filter.prod, comap_inf, comap_comap, comap_comap]
+
 lemma uniformity_prod_eq_prod [uniform_space α] [uniform_space β] :
   𝓤 (α × β) = map (λ p : (α × α) × (β × β), ((p.1.1, p.2.1), (p.1.2, p.2.2))) (𝓤 α ×ᶠ 𝓤 β) :=
-by rw [map_swap4_eq_comap, uniformity_prod, filter.prod, comap_inf, comap_comap, comap_comap]
-
-lemma mem_map_iff_exists_image' {α : Type*} {β : Type*} {f : filter α} {m : α → β} {t : set β} :
-  t ∈ (map m f).sets ↔ (∃s∈f, m '' s ⊆ t) :=
-mem_map_iff_exists_image
+by rw [map_swap4_eq_comap, uniformity_prod_eq_comap_prod]
 
-lemma mem_uniformity_of_uniform_continuous_invariant [uniform_space α] {s:set (α×α)} {f : α → α → α}
-  (hf : uniform_continuous (λp:α×α, f p.1 p.2)) (hs : s ∈ 𝓤 α) :
-  ∃u∈𝓤 α, ∀a b c, (a, b) ∈ u → (f a c, f b c) ∈ s :=
+lemma mem_uniformity_of_uniform_continuous_invariant [uniform_space α] [uniform_space β]
+  {s : set (β × β)} {f : α → α → β} (hf : uniform_continuous (λ p : α × α, f p.1 p.2))
+  (hs : s ∈ 𝓤 β) :
+  ∃ u ∈ 𝓤 α, ∀ a b c, (a, b) ∈ u → (f a c, f b c) ∈ s :=
 begin
   rw [uniform_continuous, uniformity_prod_eq_prod, tendsto_map'_iff, (∘)] at hf,
-  rcases mem_map_iff_exists_image'.1 (hf hs) with ⟨t, ht, hts⟩, clear hf,
-  rcases mem_prod_iff.1 ht with ⟨u, hu, v, hv, huvt⟩, clear ht,
-  refine ⟨u, hu, assume a b c hab, hts $ (mem_image _ _ _).2 ⟨⟨⟨a, b⟩, ⟨c, c⟩⟩, huvt ⟨_, _⟩, _⟩⟩,
-  exact hab,
-  exact refl_mem_uniformity hv,
-  refl
+  rcases mem_prod_iff.1 (mem_map.1 $ hf hs) with ⟨u, hu, v, hv, huvt⟩,
+  exact ⟨u, hu, λ a b c hab, @huvt ((_, _), (_, _)) ⟨hab, refl_mem_uniformity hv⟩⟩
 end
 
 lemma mem_uniform_prod [t₁ : uniform_space α] [t₂ : uniform_space β] {a : set (α × α)}

src/topology/uniform_space/compact_separated.lean

@@ -1,22 +1,25 @@
 /-
 Copyright (c) 2020 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Patrick Massot
+Authors: Patrick Massot, Yury Kudryashov
 -/
-import topology.uniform_space.separation
 import topology.uniform_space.uniform_convergence
+import topology.separation
+
 /-!
 # Compact separated uniform spaces
 
 ## Main statements
 
-* `compact_space_uniformity`: On a separated compact uniform space, the topology determines the
+* `compact_space_uniformity`: On a compact uniform space, the topology determines the
   uniform structure, entourages are exactly the neighborhoods of the diagonal.
+
 * `uniform_space_of_compact_t2`: every compact T2 topological structure is induced by a uniform
   structure. This uniform structure is described in the previous item.
-* Heine-Cantor theorem: continuous functions on compact separated uniform spaces with values in
-  uniform spaces are automatically uniformly continuous. There are several variations, the main one
-  is `compact_space.uniform_continuous_of_continuous`.
+
+* **Heine-Cantor** theorem: continuous functions on compact uniform spaces with values in uniform
+  spaces are automatically uniformly continuous. There are several variations, the main one is
+  `compact_space.uniform_continuous_of_continuous`.
 
 ## Implementation notes
 
@@ -33,51 +36,40 @@ open filter uniform_space set
 
 variables {α β γ : Type*} [uniform_space α] [uniform_space β]
 
-
 /-!
-### Uniformity on compact separated spaces
+### Uniformity on compact spaces
 -/
 
-/-- On a separated compact uniform space, the topology determines the uniform structure, entourages
-are exactly the neighborhoods of the diagonal. -/
-lemma compact_space_uniformity [compact_space α] [separated_space α] : 𝓤 α = ⨆ x : α, 𝓝 (x, x) :=
+/-- On a compact uniform space, the topology determines the uniform structure, entourages are
+exactly the neighborhoods of the diagonal. -/
+lemma nhds_set_diagonal_eq_uniformity [compact_space α] : 𝓝ˢ (diagonal α) = 𝓤 α :=
 begin
-  symmetry, refine le_antisymm supr_nhds_le_uniformity _,
-  by_contra H,
-  obtain ⟨V, hV, h⟩ : ∃ V : set (α × α), (∀ x : α, V ∈ 𝓝 (x, x)) ∧ 𝓤 α ⊓ 𝓟 Vᶜ ≠ ⊥,
-  { simpa only [le_iff_forall_inf_principal_compl, mem_supr, not_forall, exists_prop] using H },
-  let F := 𝓤 α ⊓ 𝓟 Vᶜ,
-  haveI : ne_bot F := ⟨h⟩,
-  obtain ⟨⟨x, y⟩, hx⟩ : ∃ (p : α × α), cluster_pt p F :=
-    cluster_point_of_compact F,
-  have : cluster_pt (x, y) (𝓤 α) :=
-    hx.of_inf_left,
-  obtain rfl : x = y := eq_of_uniformity_inf_nhds this,
-  have : cluster_pt (x, x) (𝓟 Vᶜ) :=
-   hx.of_inf_right,
-  have : (x, x) ∉ interior V,
-  { have : (x, x) ∈ closure Vᶜ, by rwa mem_closure_iff_cluster_pt,
-    rwa closure_compl at this },
-  have : (x, x) ∈ interior V,
-  { rw mem_interior_iff_mem_nhds,
-    exact hV x },
-  contradiction
+  refine nhds_set_diagonal_le_uniformity.antisymm _,
+  have : (𝓤 (α × α)).has_basis (λ U, U ∈ 𝓤 α)
+    (λ U, (λ p : (α × α) × α × α, ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U),
+  { rw [uniformity_prod_eq_comap_prod],
+    exact (𝓤 α).basis_sets.prod_self.comap _ },
+  refine (is_compact_diagonal.nhds_set_basis_uniformity this).ge_iff.2 (λ U hU, _),
+  exact mem_of_superset hU (λ ⟨x, y⟩ hxy, mem_Union₂.2 ⟨(x, x), rfl, refl_mem_uniformity hU, hxy⟩)
 end
 
-lemma unique_uniformity_of_compact_t2 [t : topological_space γ] [compact_space γ]
-[t2_space γ] {u u' : uniform_space γ}
-(h : u.to_topological_space = t) (h' : u'.to_topological_space = t) : u = u' :=
+/-- On a compact uniform space, the topology determines the uniform structure, entourages are
+exactly the neighborhoods of the diagonal. -/
+lemma compact_space_uniformity [compact_space α] : 𝓤 α = ⨆ x, 𝓝 (x, x) :=
+nhds_set_diagonal_eq_uniformity.symm.trans (nhds_set_diagonal _)
+
+lemma unique_uniformity_of_compact [t : topological_space γ] [compact_space γ]
+  {u u' : uniform_space γ} (h : u.to_topological_space = t) (h' : u'.to_topological_space = t) :
+  u = u' :=
 begin
   apply uniform_space_eq,
   change uniformity _ = uniformity _,
-  haveI : @compact_space γ u.to_topological_space, { rw h ; assumption },
-  haveI : @compact_space γ u'.to_topological_space, { rw h' ; assumption },
-  haveI : @separated_space γ u, { rwa [separated_iff_t2, h] },
-  haveI : @separated_space γ u', { rwa [separated_iff_t2, h'] },
+  haveI : @compact_space γ u.to_topological_space, { rwa h },
+  haveI : @compact_space γ u'.to_topological_space, { rwa h' },
   rw [compact_space_uniformity, compact_space_uniformity, h, h']
 end
 
-/-- The unique uniform structure inducing a given compact Hausdorff topological structure. -/
+/-- The unique uniform structure inducing a given compact topological structure. -/
 def uniform_space_of_compact_t2 [topological_space γ] [compact_space γ] [t2_space γ] :
   uniform_space γ :=
 { uniformity := ⨆ x, 𝓝 (x, x),
@@ -188,7 +180,7 @@ def uniform_space_of_compact_t2 [topological_space γ] [compact_space γ] [t2_sp
 
 /-- Heine-Cantor: a continuous function on a compact separated uniform space is uniformly
 continuous. -/
-lemma compact_space.uniform_continuous_of_continuous [compact_space α] [separated_space α]
+lemma compact_space.uniform_continuous_of_continuous [compact_space α]
   {f : α → β} (h : continuous f) : uniform_continuous f :=
 calc
 map (prod.map f f) (𝓤 α) = map (prod.map f f) (⨆ x, 𝓝 (x, x))  : by rw compact_space_uniformity
@@ -197,44 +189,34 @@ map (prod.map f f) (𝓤 α) = map (prod.map f f) (⨆ x, 𝓝 (x, x))  : by rw
                      ... ≤ ⨆ y, 𝓝 (y, y)         : supr_comp_le (λ y, 𝓝 (y, y)) f
                      ... ≤ 𝓤 β                   : supr_nhds_le_uniformity
 
-/-- Heine-Cantor: a continuous function on a compact separated set of a uniform space is
-uniformly continuous. -/
-lemma is_compact.uniform_continuous_on_of_continuous' {s : set α} {f : α → β}
-  (hs : is_compact s) (hs' : is_separated s) (hf : continuous_on f s) : uniform_continuous_on f s :=
+/-- Heine-Cantor: a continuous function on a compact set of a uniform space is uniformly
+continuous. -/
+lemma is_compact.uniform_continuous_on_of_continuous {s : set α} {f : α → β}
+  (hs : is_compact s) (hf : continuous_on f s) : uniform_continuous_on f s :=
 begin
   rw uniform_continuous_on_iff_restrict,
-  rw is_separated_iff_induced at hs',
   rw is_compact_iff_compact_space at hs,
   rw continuous_on_iff_continuous_restrict at hf,
   resetI,
   exact compact_space.uniform_continuous_of_continuous hf,
 end
 
-/-- Heine-Cantor: a continuous function on a compact set of a separated uniform space
-is uniformly continuous. -/
-lemma is_compact.uniform_continuous_on_of_continuous [separated_space α] {s : set α} {f : α → β}
-  (hs : is_compact s) (hf : continuous_on f s) : uniform_continuous_on f s :=
-hs.uniform_continuous_on_of_continuous' (is_separated_of_separated_space s) hf
-
 /-- A family of functions `α → β → γ` tends uniformly to its value at `x` if `α` is locally compact,
-`β` is compact and separated and `f` is continuous on `U × (univ : set β)` for some separated
-neighborhood `U` of `x`. -/
+`β` is compact and `f` is continuous on `U × (univ : set β)` for some neighborhood `U` of `x`. -/
 lemma continuous_on.tendsto_uniformly [locally_compact_space α] [compact_space β]
-  [separated_space β] [uniform_space γ] {f : α → β → γ} {x : α} {U : set α}
-  (hxU : U ∈ 𝓝 x) (hU : is_separated U) (h : continuous_on ↿f (U ×ˢ univ)) :
+  [uniform_space γ] {f : α → β → γ} {x : α} {U : set α}
+  (hxU : U ∈ 𝓝 x) (h : continuous_on ↿f (U ×ˢ univ)) :
   tendsto_uniformly f (f x) (𝓝 x) :=
 begin
   rcases locally_compact_space.local_compact_nhds _ _ hxU with ⟨K, hxK, hKU, hK⟩,
   have : uniform_continuous_on ↿f (K ×ˢ univ),
-  { refine is_compact.uniform_continuous_on_of_continuous' (hK.prod compact_univ) _
+    from is_compact.uniform_continuous_on_of_continuous (hK.prod compact_univ)
       (h.mono $ prod_mono hKU subset.rfl),
-    exact (hU.mono hKU).prod (is_separated_of_separated_space _) },
   exact this.tendsto_uniformly hxK
 end
 
 /-- A continuous family of functions `α → β → γ` tends uniformly to its value at `x` if `α` is
-locally compact and `β` is compact and separated. -/
-lemma continuous.tendsto_uniformly [separated_space α] [locally_compact_space α]
-  [compact_space β] [separated_space β] [uniform_space γ]
+locally compact and `β` is compact. -/
+lemma continuous.tendsto_uniformly [locally_compact_space α] [compact_space β] [uniform_space γ]
   (f : α → β → γ) (h : continuous ↿f) (x : α) : tendsto_uniformly f (f x) (𝓝 x) :=
-h.continuous_on.tendsto_uniformly univ_mem $ is_separated_of_separated_space _
+h.continuous_on.tendsto_uniformly univ_mem