chore(*): last preparations for Heine (#3179)

This is hopefully the last preparatory PR before we study compact uniform spaces. It has almost no mathematical content, except that I define `uniform_continuous_on`, and check it is equivalent to uniform continuity for the induced uniformity.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: PatrickMassot

src/data/set/basic.lean

@@ -346,6 +346,10 @@ instance univ_decidable : decidable_pred (@set.univ α) :=
 /-- `diagonal α` is the subset of `α × α` consisting of all pairs of the form `(a, a)`. -/
 def diagonal (α : Type*) : set (α × α) := {p | p.1 = p.2}
 
+@[simp]
+lemma mem_diagonal {α : Type*} (x : α) : (x, x) ∈ diagonal α :=
+by simp [diagonal]
+
 /-! ### Lemmas about union -/
 
 theorem union_def {s₁ s₂ : set α} : s₁ ∪ s₂ = {a | a ∈ s₁ ∨ a ∈ s₂} := rfl
@@ -1449,6 +1453,9 @@ range_subset_iff.2 $ λ x, rfl
 | ⟨x⟩ c := subset.antisymm range_const_subset $
   assume y hy, (mem_singleton_iff.1 hy).symm ▸ mem_range_self x
 
+lemma diagonal_eq_range {α  : Type*} : diagonal α = range (λ x, (x, x)) :=
+by { ext ⟨x, y⟩, simp [diagonal, eq_comm] }
+
 theorem preimage_singleton_nonempty {f : α → β} {y : β} :
   (f ⁻¹' {y}).nonempty ↔ y ∈ range f :=
 iff.rfl

src/order/complete_lattice.lean

@@ -641,6 +641,14 @@ theorem infi_union {f : β → α} {s t : set β} : (⨅ x ∈ s ∪ t, f x) = (
 calc (⨅ x ∈ s ∪ t, f x) = (⨅ x, (⨅h : x∈s, f x) ⊓ (⨅h : x∈t, f x)) : congr_arg infi $ funext $ assume x, infi_or
                     ... = (⨅x∈s, f x) ⊓ (⨅x∈t, f x) : infi_inf_eq
 
+lemma infi_split (f : β → α) (p : β → Prop) :
+  (⨅ i, f i) = (⨅ i (h : p i), f i) ⊓ (⨅ i (h : ¬ p i), f i) :=
+by simpa [classical.em] using @infi_union _ _ _ f {i | p i} {i | ¬ p i}
+
+lemma infi_split_single (f : β → α) (i₀ : β) :
+  (⨅ i, f i) = f i₀ ⊓ (⨅ i (h : i ≠ i₀), f i) :=
+by convert infi_split _ _; simp
+
 theorem infi_le_infi_of_subset {f : β → α} {s t : set β} (h : s ⊆ t) :
   (⨅ x ∈ t, f x) ≤ (⨅ x ∈ s, f x) :=
 by rw [(union_eq_self_of_subset_left h).symm, infi_union]; exact inf_le_left
@@ -649,6 +657,14 @@ theorem supr_union {f : β → α} {s t : set β} : (⨆ x ∈ s ∪ t, f x) = (
 calc (⨆ x ∈ s ∪ t, f x) = (⨆ x, (⨆h : x∈s, f x) ⊔ (⨆h : x∈t, f x)) : congr_arg supr $ funext $ assume x, supr_or
                     ... = (⨆x∈s, f x) ⊔ (⨆x∈t, f x) : supr_sup_eq
 
+lemma supr_split (f : β → α) (p : β → Prop) :
+  (⨆ i, f i) = (⨆ i (h : p i), f i) ⊔ (⨆ i (h : ¬ p i), f i) :=
+by simpa [classical.em] using @supr_union _ _ _ f {i | p i} {i | ¬ p i}
+
+lemma supr_split_single (f : β → α) (i₀ : β) :
+  (⨆ i, f i) = f i₀ ⊔ (⨆ i (h : i ≠ i₀), f i) :=
+by convert supr_split _ _; simp
+
 theorem supr_le_supr_of_subset {f : β → α} {s t : set β} (h : s ⊆ t) :
   (⨆ x ∈ s, f x) ≤ (⨆ x ∈ t, f x) :=
 by rw [(union_eq_self_of_subset_left h).symm, supr_union]; exact le_sup_left

src/order/filter/basic.lean

@@ -751,6 +751,38 @@ begin
   refl
 end
 
+lemma mem_iff_inf_principal_compl {f : filter α} {V : set α} :
+  V ∈ f ↔ f ⊓ 𝓟 (-V) = ⊥ :=
+begin
+  rw inf_eq_bot_iff,
+  split,
+  { intro h,
+    use [V, -V],
+    simp [h, subset.refl] },
+  { rintros ⟨U, W, U_in, W_in, UW⟩,
+    rw [mem_principal_sets, compl_subset_comm] at W_in,
+    apply mem_sets_of_superset U_in,
+    intros x x_in,
+    apply W_in,
+    intro H,
+    have : x ∈ U ∩ W := ⟨x_in, H⟩,
+    rwa UW at this },
+end
+
+lemma le_iff_forall_inf_principal_compl {f g : filter α} :
+  f ≤ g ↔ ∀ V ∈ g, f ⊓ 𝓟 (-V) = ⊥ :=
+begin
+  change (∀ V ∈ g, V ∈ f) ↔ _,
+  simp_rw [mem_iff_inf_principal_compl],
+end
+
+lemma principal_le_iff {s : set α} {f : filter α} :
+  𝓟 s ≤ f ↔ ∀ V ∈ f, s ⊆ V :=
+begin
+  change (∀ V, V ∈ f → V ∈ _) ↔ _,
+  simp_rw mem_principal_sets,
+end
+
 @[simp] lemma infi_principal_finset {ι : Type w} (s : finset ι) (f : ι → set α) :
   (⨅i∈s, 𝓟 (f i)) = 𝓟 (⋂i∈s, f i) :=
 begin
@@ -1259,6 +1291,28 @@ theorem preimage_mem_comap (ht : t ∈ g) : m ⁻¹' t ∈ comap m g :=
 lemma comap_id : comap id f = f :=
 le_antisymm (assume s, preimage_mem_comap) (assume s ⟨t, ht, hst⟩, mem_sets_of_superset ht hst)
 
+lemma comap_const_of_not_mem {x : α} {f : filter α} {V : set α} (hV : V ∈ f) (hx : x ∉ V) :
+  comap (λ y : α, x) f = ⊥ :=
+begin
+  ext W,
+  suffices : ∃ t ∈ f, (λ (y : α), x) ⁻¹' t ⊆ W, by simpa,
+  use [V, hV],
+  simp [preimage_const_of_not_mem hx],
+end
+
+lemma comap_const_of_mem {x : α} {f : filter α} (h : ∀ V ∈ f, x ∈ V) : comap (λ y : α, x) f = ⊤ :=
+begin
+  ext W,
+  suffices : (∃ (t : set α), t ∈ f.sets ∧ (λ (y : α), x) ⁻¹' t ⊆ W) ↔ W = univ,
+  by simpa,
+  split,
+  { rintros ⟨V, V_in, hW⟩,
+    simpa [preimage_const_of_mem (h V V_in),  univ_subset_iff] using hW },
+  { rintro rfl,
+    use univ,
+    simp [univ_mem_sets] },
+end
+
 lemma comap_comap_comp {m : γ → β} {n : β → α} : comap m (comap n f) = comap (n ∘ m) f :=
 le_antisymm
   (assume c ⟨b, hb, (h : preimage (n ∘ m) b ⊆ c)⟩, ⟨preimage n b, preimage_mem_comap hb, h⟩)
@@ -1403,6 +1457,17 @@ begin
     exact H }
 end
 
+lemma subtype_coe_map_comap_prod (s : set α) (f : filter (α × α)) :
+  map (coe : s × s → α × α) (comap (coe : s × s → α × α) f) = f ⊓ 𝓟 (s.prod s) :=
+let φ (x : s × s) : s.prod s := ⟨⟨x.1.1, x.2.1⟩, ⟨x.1.2, x.2.2⟩⟩ in
+begin
+  rw show (coe : s × s → α × α) = coe ∘ φ, by ext x; cases x; refl,
+  rw [← filter.map_map, ← filter.comap_comap_comp],
+  rw map_comap_of_surjective,
+  exact subtype_coe_map_comap _ _,
+  exact λ ⟨⟨a, b⟩, ⟨ha, hb⟩⟩, ⟨⟨⟨a, ha⟩, ⟨b, hb⟩⟩, rfl⟩
+end
+
 lemma comap_ne_bot {f : filter β} {m : α → β} (hm : ∀t∈ f, ∃a, m a ∈ t) :
   comap m f ≠ ⊥ :=
 forall_sets_nonempty_iff_ne_bot.mp $ assume s ⟨t, ht, t_s⟩,
@@ -1923,6 +1988,10 @@ begin
     ⟨prod.fst ⁻¹' t₁, ⟨t₁, ht₁, subset.refl _⟩, prod.snd ⁻¹' t₂, ⟨t₂, ht₂, subset.refl _⟩, h⟩
 end
 
+lemma comap_prod (f : α → β × γ) (b : filter β) (c : filter γ) :
+  comap f (b ×ᶠ c) = (comap (prod.fst ∘ f) b) ⊓ (comap (prod.snd ∘ f) c) :=
+by erw [comap_inf, filter.comap_comap_comp, filter.comap_comap_comp]
+
 lemma eventually_prod_iff {p : α × β → Prop} {f : filter α} {g : filter β} :
   (∀ᶠ x in f ×ᶠ g, p x) ↔ ∃ (pa : α → Prop) (ha : ∀ᶠ x in f, pa x)
     (pb : β → Prop) (hb : ∀ᶠ y in g, pb y), ∀ {x}, pa x → ∀ {y}, pb y → p (x, y) :=

src/topology/basic.lean

@@ -525,6 +525,10 @@ In this section we define [cluster points](https://en.wikipedia.org/wiki/Limit_p
 an accumulation point or a limit point. -/
 def cluster_pt (x : α) (F : filter α) : Prop := 𝓝 x ⊓ F ≠ ⊥
 
+lemma cluster_pt_iff {x : α} {F : filter α} :
+  cluster_pt x F ↔ ∀ {U V : set α}, U ∈ 𝓝 x → V ∈ F → (U ∩ V).nonempty :=
+by rw [cluster_pt, inf_ne_bot_iff]
+
 lemma cluster_pt.of_le_nhds {x : α} {f : filter α} (H : f ≤ 𝓝 x) (h : f ≠ ⊥) : cluster_pt x f :=
 by rwa [cluster_pt, inf_comm, inf_eq_left.mpr H]
 
@@ -535,11 +539,11 @@ lemma cluster_pt.mono {x : α} {f g : filter α} (H : cluster_pt x f) (h : f ≤
   cluster_pt x g :=
 ne_bot_of_le_ne_bot H $ inf_le_inf_left _ h
 
-lemma cluster_pt_of_inf_left {x : α} {f g : filter α} (H : cluster_pt x $ f ⊓ g) :
+lemma cluster_pt.of_inf_left {x : α} {f g : filter α} (H : cluster_pt x $ f ⊓ g) :
   cluster_pt x f :=
 H.mono inf_le_left
 
-lemma cluster_pt_of_inf_right {x : α} {f g : filter α} (H : cluster_pt x $ f ⊓ g) :
+lemma cluster_pt.of_inf_right {x : α} {f g : filter α} (H : cluster_pt x $ f ⊓ g) :
   cluster_pt x g :=
 H.mono inf_le_right
 
@@ -574,6 +578,9 @@ lemma mem_interior_iff_mem_nhds {s : set α} {a : α} :
   a ∈ interior s ↔ s ∈ 𝓝 a :=
 by simp only [interior_eq_nhds, le_principal_iff]; refl
 
+lemma subset_interior_iff_nhds {s V : set α} : s ⊆ interior V ↔ ∀ x ∈ s, V ∈ 𝓝 x :=
+show (∀ x, x ∈ s →  x ∈ _) ↔ _, by simp_rw mem_interior_iff_mem_nhds
+
 lemma is_open_iff_nhds {s : set α} : is_open s ↔ ∀a∈s, 𝓝 a ≤ 𝓟 s :=
 calc is_open s ↔ s ⊆ interior s : subset_interior_iff_open.symm
   ... ↔ (∀a∈s, 𝓝 a ≤ 𝓟 s) : by rw [interior_eq_nhds]; refl
@@ -589,6 +596,9 @@ calc closure s = - interior (- s) : closure_eq_compl_interior_compl
       (show 𝓟 s ⊔ 𝓟 (-s) = ⊤, by simp only [sup_principal, union_compl_self, principal_univ])
       (by simp only [inf_principal, inter_compl_self, principal_empty])).symm
 
+theorem mem_closure_iff_cluster_pt {s : set α} {a : α} : a ∈ closure s ↔ cluster_pt a (𝓟 s) :=
+by simpa only [closure_eq_cluster_pts]
+
 theorem mem_closure_iff_nhds {s : set α} {a : α} :
   a ∈ closure s ↔ ∀ t ∈ 𝓝 a, (t ∩ s).nonempty :=
 mem_closure_iff.trans

src/topology/metric_space/basic.lean

@@ -418,6 +418,16 @@ theorem uniform_continuous_iff [metric_space β] {f : α → β} :
     ∀{a b:α}, dist a b < δ → dist (f a) (f b) < ε :=
 uniformity_basis_dist.uniform_continuous_iff uniformity_basis_dist
 
+@[nolint ge_or_gt] -- see Note [nolint_ge]
+lemma uniform_continuous_on_iff [metric_space β] {f : α → β} {s : set α} :
+  uniform_continuous_on f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ x y ∈ s, dist x y < δ → dist (f x) (f y) < ε :=
+begin
+  dsimp [uniform_continuous_on],
+  rw (metric.uniformity_basis_dist.inf_principal (s.prod s)).tendsto_iff metric.uniformity_basis_dist,
+  simp only [and_imp, exists_prop, prod.forall, mem_inter_eq, gt_iff_lt, mem_set_of_eq, mem_prod],
+  finish,
+end
+
 @[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem uniform_embedding_iff [metric_space β] {f : α → β} :
   uniform_embedding f ↔ function.injective f ∧ uniform_continuous f ∧
@@ -531,13 +541,15 @@ lemma tendsto_uniformly_iff {ι : Type*}
   tendsto_uniformly F f p ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x, dist (f x) (F n x) < ε :=
 by { rw [← tendsto_uniformly_on_univ, tendsto_uniformly_on_iff], simp }
 
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 protected lemma cauchy_iff {f : filter α} :
   cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x y ∈ t, dist x y < ε :=
 uniformity_basis_dist.cauchy_iff
 
 theorem nhds_basis_ball : (𝓝 x).has_basis (λ ε:ℝ, 0 < ε) (ball x) :=
 nhds_basis_uniformity uniformity_basis_dist
 
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem mem_nhds_iff : s ∈ 𝓝 x ↔ ∃ε>0, ball x ε ⊆ s :=
 nhds_basis_ball.mem_iff
 
@@ -552,6 +564,7 @@ theorem nhds_basis_ball_inv_nat_pos :
   (𝓝 x).has_basis (λ n, 0<n) (λ n:ℕ, ball x (1 / ↑n)) :=
 nhds_basis_uniformity uniformity_basis_dist_inv_nat_pos
 
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem is_open_iff : is_open s ↔ ∀x∈s, ∃ε>0, ball x ε ⊆ s :=
 by simp only [is_open_iff_mem_nhds, mem_nhds_iff]
 
@@ -613,6 +626,7 @@ theorem continuous_iff [metric_space β] {f : α → β} :
   ∀b (ε > 0), ∃ δ > 0, ∀a, dist a b < δ → dist (f a) (f b) < ε :=
 continuous_iff_continuous_at.trans $ forall_congr $ λ b, tendsto_nhds_nhds
 
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem tendsto_nhds {f : filter β} {u : β → α} {a : α} :
   tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ x in f, dist (u x) a < ε :=
 nhds_basis_ball.tendsto_right_iff
@@ -717,6 +731,10 @@ lemma metric.emetric_closed_ball_nnreal {x : α} {ε : nnreal} :
   emetric.closed_ball x ε = closed_ball x ε :=
 by { convert metric.emetric_closed_ball ε.2, simp }
 
+/-- Build a new metric space from an old one where the bundled uniform structure is provably
+(but typically non-definitionaly) equal to some given uniform structure.
+See Note [forgetful inheritance].
+-/
 def metric_space.replace_uniformity {α} [U : uniform_space α] (m : metric_space α)
   (H : @uniformity _ U = @uniformity _ emetric_space.to_uniform_space') :
   metric_space α :=
@@ -934,6 +952,8 @@ lemma cauchy_seq_iff_le_tendsto_0 {s : ℕ → α} : cauchy_seq s ↔ ∃ b : 
 
 end cauchy_seq
 
+/-- Metric space structure pulled back by an injective function. Injectivity is necessary to
+ensure that `dist x y = 0` only if `x = y`. -/
 def metric_space.induced {α β} (f : α → β) (hf : function.injective f)
   (m : metric_space β) : metric_space α :=
 { dist               := λ x y, dist (f x) (f y),

src/topology/separation.lean

@@ -335,6 +335,20 @@ let ⟨s, hs, hys, hxs⟩ := regular_space.regular is_closed_singleton
 ⟨v, s, hv, hs, hxv, singleton_subset_iff.1 hys,
 eq_empty_of_subset_empty $ λ z ⟨hzv, hzs⟩, htu ⟨hvt hzv, hsu hzs⟩⟩⟩
 
+variable {α}
+
+lemma disjoint_nested_nhds [regular_space α] {x y : α} (h : x ≠ y) :
+  ∃ (U₁ V₁ ∈ 𝓝 x) (U₂ V₂ ∈ 𝓝 y), is_closed V₁ ∧ is_closed V₂ ∧ is_open U₁ ∧ is_open U₂ ∧
+  V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ U₁ ∩ U₂ = ∅ :=
+begin
+  rcases t2_separation h with ⟨U₁, U₂, U₁_op, U₂_op, x_in, y_in, H⟩,
+  rcases nhds_is_closed (mem_nhds_sets U₁_op x_in) with ⟨V₁, V₁_in, h₁, V₁_closed⟩,
+  rcases nhds_is_closed (mem_nhds_sets U₂_op y_in) with ⟨V₂, V₂_in, h₂, V₂_closed⟩,
+  use [U₁, V₁, mem_sets_of_superset V₁_in h₁, V₁_in,
+       U₂, V₂, mem_sets_of_superset V₂_in h₂, V₂_in],
+  tauto
+end
+
 end regularity
 
 section normality

src/topology/subset_properties.lean

@@ -66,13 +66,13 @@ classical.by_cases mem_sets_of_eq_bot $
   assume : f ⊓ 𝓟 (- t) ≠ ⊥,
   let ⟨a, ha, (hfa : cluster_pt a $ f ⊓ 𝓟 (-t))⟩ := hs _ this $ inf_le_left_of_le hf₂ in
   have a ∈ t,
-    from ht₂ a ha (cluster_pt_of_inf_left hfa),
+    from ht₂ a ha (hfa.of_inf_left),
   have (-t) ∩ t ∈ nhds_within a (-t),
     from inter_mem_nhds_within _ (mem_nhds_sets ht₁ this),
   have A : nhds_within a (-t) = ⊥,
     from empty_in_sets_eq_bot.1 $ compl_inter_self t ▸ this,
   have nhds_within a (-t) ≠ ⊥,
-    from cluster_pt_of_inf_right hfa,
+    from hfa.of_inf_right,
   absurd A this
 
 lemma compact_iff_ultrafilter_le_nhds {s : set α} :

src/topology/uniform_space/basic.lean

@@ -550,12 +550,17 @@ lemma mem_nhds_uniformity_iff_left {x : α} {s : set α} :
   s ∈ 𝓝 x ↔ {p : α × α | p.2 = x → p.1 ∈ s} ∈ 𝓤 α :=
 by { rw [uniformity_eq_symm, mem_nhds_uniformity_iff_right], refl }
 
-lemma nhds_eq_comap_uniformity {x : α} : 𝓝 x = (𝓤 α).comap (prod.mk x) :=
-by ext s; rw [mem_nhds_uniformity_iff_right, mem_comap_sets]; from iff.intro
+lemma nhds_eq_comap_uniformity_aux  {α : Type u} {x : α} {s : set α} {F : filter (α × α)} :
+  {p : α × α | p.fst = x → p.snd ∈ s} ∈ F ↔ s ∈ comap (prod.mk x) F :=
+by rw mem_comap_sets ; from iff.intro
   (assume hs, ⟨_, hs, assume x hx, hx rfl⟩)
-  (assume ⟨t, h, ht⟩, (𝓤 α).sets_of_superset h $
+  (assume ⟨t, h, ht⟩, F.sets_of_superset h $
     assume ⟨p₁, p₂⟩ hp (h : p₁ = x), ht $ by simp [h.symm, hp])
 
+
+lemma nhds_eq_comap_uniformity {x : α} : 𝓝 x = (𝓤 α).comap (prod.mk x) :=
+by { ext s, rw [mem_nhds_uniformity_iff_right], exact nhds_eq_comap_uniformity_aux }
+
 lemma is_open_iff_ball_subset {s : set α} : is_open s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s :=
 begin
   simp_rw [is_open_iff_mem_nhds, nhds_eq_comap_uniformity],
@@ -695,6 +700,20 @@ match this with
     Union_subset $ assume p, Union_subset $ assume hp, (ht p hp).left⟩
 end
 
+/-- Entourages are neighborhoods of the diagonal. -/
+lemma nhds_le_uniformity : (⨆ x : α, 𝓝 (x, x)) ≤ 𝓤 α :=
+begin
+  apply supr_le _,
+  intros x V V_in,
+  rcases comp_symm_mem_uniformity_sets V_in with ⟨w, w_in, w_symm, w_sub⟩,
+  have : (ball x w).prod (ball x w) ∈ 𝓝 (x, x),
+  { rw nhds_prod_eq,
+    exact prod_mem_prod (ball_mem_nhds x w_in) (ball_mem_nhds x w_in) },
+  apply mem_sets_of_superset this,
+  rintros ⟨u, v⟩ ⟨u_in, v_in⟩,
+  exact w_sub (mem_comp_of_mem_ball w_symm u_in v_in)
+end
+
 /-!
 ### Closure and interior in uniform spaces
 -/
@@ -851,6 +870,13 @@ as `(x, y)` tends to the diagonal. In other words, if `x` is sufficiently close
 def uniform_continuous [uniform_space β] (f : α → β) :=
 tendsto (λx:α×α, (f x.1, f x.2)) (𝓤 α) (𝓤 β)
 
+/-- A function `f : α → β` is *uniformly continuous* on `s : set α` if `(f x, f y)` tends to
+the diagonal as `(x, y)` tends to the diagonal while remaining in `s.prod s`.
+In other words, if `x` is sufficiently close to `y`, then `f x` is close to
+`f y` no matter where `x` and `y` are located in `s`.-/
+def uniform_continuous_on [uniform_space β] (f : α → β) (s : set α) : Prop :=
+tendsto (λ x : α × α, (f x.1, f x.2)) (𝓤 α ⊓ principal (s.prod s)) (𝓤 β)
+
 theorem uniform_continuous_def [uniform_space β] {f : α → β} :
   uniform_continuous f ↔ ∀ r ∈ 𝓤 β, { x : α × α | (f x.1, f x.2) ∈ r} ∈ 𝓤 α :=
 iff.rfl
@@ -1096,6 +1122,17 @@ lemma uniform_continuous_subtype_mk {p : α → Prop} [uniform_space α] [unifor
   uniform_continuous (λx, ⟨f x, h x⟩ : β → subtype p) :=
 uniform_continuous_comap' hf
 
+lemma uniform_continuous_on_iff_restrict [uniform_space α] [uniform_space β] (f : α → β) (s : set α) :
+  uniform_continuous_on f s ↔ uniform_continuous (s.restrict f) :=
+begin
+  unfold uniform_continuous_on set.restrict uniform_continuous tendsto,
+  rw [show (λ x : s × s, (f x.1, f x.2)) = prod.map f f ∘ coe, by ext x; cases x; refl,
+      uniformity_comap rfl,
+      show prod.map subtype.val subtype.val = (coe : s × s → α × α), by ext x; cases x; refl],
+  conv in (map _ (comap _ _)) { rw ← filter.map_map },
+  rw subtype_coe_map_comap_prod, refl,
+end
+
 lemma tendsto_of_uniform_continuous_subtype
   [uniform_space α] [uniform_space β] {f : α → β} {s : set α} {a : α}
   (hf : uniform_continuous (λx:s, f x.val)) (ha : s ∈ 𝓝 a) :