From 279173913e368987ab8fc27a9f5097466d9cd8c5 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 11 Sep 2022 19:22:57 +0000 Subject: [PATCH] feat(topology/uniform_space/compact_separated): drop unneeded assumptions (#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 | 7 +- src/topology/nhds_set.lean | 3 + src/topology/subset_properties.lean | 3 + src/topology/uniform_space/basic.lean | 57 +++++++--- .../uniform_space/compact_separated.lean | 104 ++++++++---------- 5 files changed, 95 insertions(+), 79 deletions(-) diff --git a/src/topology/algebra/uniform_group.lean b/src/topology/algebra/uniform_group.lean index 1833669c5c04b..af3ad1cdbdeea 100644 --- a/src/topology/algebra/uniform_group.lean +++ b/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⟩ diff --git a/src/topology/nhds_set.lean b/src/topology/nhds_set.lean index 907437b3152ed..04fc5c72a962b 100644 --- a/src/topology/nhds_set.lean +++ b/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] diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean index 8dbe23d765f0b..627d55a1d3044 100644 --- a/src/topology/subset_properties.lean +++ b/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] diff --git a/src/topology/uniform_space/basic.lean b/src/topology/uniform_space/basic.lean index fe33e6b76513c..22e1275bd01b6 100644 --- a/src/topology/uniform_space/basic.lean +++ b/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 (α × α)} diff --git a/src/topology/uniform_space/compact_separated.lean b/src/topology/uniform_space/compact_separated.lean index d610588238d57..9fddded951809 100644 --- a/src/topology/uniform_space/compact_separated.lean +++ b/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