feat(topology/uniform_space/uniform_convergence_topology): bases for …

…uniform structures of 𝔖-convergence (#14778)

By definition, the sets `S(V) := {(f, g) | ∀ x, (f x, g x) ∈ V}` for `V∈𝓤 β` form a basis for the uniformity of uniform convergence on `α → β`. We extend this result in the two following ways : 
- we show that it suffices to consider only the sets `V` in a basis of `𝓤 β` instead of all the entourages
- we deduce a similar result for the uniformity of 𝔖-convergence for a directed 𝔖 : in that case, a basis is given by the sets `S'(A,V) := {(f, g) | ∀ x ∈ A, (f x, g x) ∈ V}` for `A ∈𝔖` and `V` in a basis of `𝓤 β`

src/topology/uniform_space/uniform_convergence_topology.lean

@@ -231,16 +231,32 @@ protected lemma has_basis_uniformity :
   (uniform_convergence.gen α β) :=
 (uniform_convergence.is_basis_gen α β (𝓤 β)).has_basis
 
+/-- The uniformity of `α → β` endowed with the uniform structure of uniform convergence on admits
+the family `{(f, g) | ∀ x, (f x, g x) ∈ V}` for `V ∈ 𝓑` as a filter basis, for any basis
+`𝓑` of `𝓤 β` (in the case `𝓑 = (𝓤 β).as_basis` this is true by definition). -/
+protected lemma has_basis_uniformity_of_basis {ι : Sort*} {p : ι → Prop} {s : ι → set (β × β)}
+  (h : (𝓤 β).has_basis p s) :
+  (𝓤 (α → β)).has_basis p (uniform_convergence.gen α β ∘ s) :=
+(uniform_convergence.has_basis_uniformity α β).to_has_basis
+  (λ U hU, let ⟨i, hi, hiU⟩ := h.mem_iff.mp hU in ⟨i, hi, λ uv huv x, hiU (huv x)⟩)
+  (λ i hi, ⟨s i, h.mem_of_mem hi, subset_refl _⟩)
+
 /-- Topology of uniform convergence. -/
 protected def topological_space : topological_space (α → β) :=
 (𝒰(α, β, infer_instance)).to_topological_space
 
+/-- If `α → β` is endowed with the topology of uniform convergence, `𝓝 f` admits the family
+`{g | ∀ x, (f x, g x) ∈ V}` for `V ∈ 𝓑` as a filter basis, for any basis `𝓑` of `𝓤 β`. -/
+protected lemma has_basis_nhds_of_basis (f) {p : ι → Prop} {s : ι → set (β × β)}
+  (h : has_basis (𝓤 β) p s) :
+  (𝓝 f).has_basis p (λ i, {g | (f, g) ∈ uniform_convergence.gen α β (s i)}) :=
+nhds_basis_uniformity' (uniform_convergence.has_basis_uniformity_of_basis α β h)
+
 /-- If `α → β` is endowed with the topology of uniform convergence, `𝓝 f` admits the family
 `{g | ∀ x, (f x, g x) ∈ V}` for `V ∈ 𝓤 β` as a filter basis. -/
-protected lemma has_basis_nhds :
-  (𝓝 f).has_basis (λ V, V ∈ 𝓤 β)
-  (λ V, {g | (f, g) ∈ uniform_convergence.gen α β V}) :=
-nhds_basis_uniformity' (uniform_convergence.has_basis_uniformity α β)
+protected lemma has_basis_nhds (f) :
+  (𝓝 f).has_basis (λ V, V ∈ 𝓤 β) (λ V, {g | (f, g) ∈ uniform_convergence.gen α β V}) :=
+uniform_convergence.has_basis_nhds_of_basis α β f (filter.basis_sets _)
 
 variables {α}
 
@@ -407,7 +423,7 @@ end
 protected lemma tendsto_iff_tendsto_uniformly : tendsto F p (𝓝 f) ↔ tendsto_uniformly F f p :=
 begin
   letI : uniform_space (α → β) := 𝒰(α, β, _),
-  rw [(uniform_convergence.has_basis_nhds α β).tendsto_right_iff, tendsto_uniformly],
+  rw [(uniform_convergence.has_basis_nhds α β f).tendsto_right_iff, tendsto_uniformly],
   exact iff.rfl,
 end
 
@@ -469,11 +485,49 @@ end uniform_convergence
 
 namespace uniform_convergence_on
 
-variables (α β : Type*) {γ ι : Type*} [uniform_space β] (𝔖 : set (set α))
+variables {α β : Type*} {γ ι : Type*}
 variables {F : ι → α → β} {f : α → β} {s s' : set α} {x : α} {p : filter ι} {g : ι → α}
 
 local notation `𝒰(`α`, `β`, `u`)` := @uniform_convergence.uniform_space α β u
 
+/-- Basis sets for the uniformity of `𝔖`-convergence: for `S : set α` and `V : set (β × β)`,
+`gen S V` is the set of pairs `(f, g)` of functions `α → β` such that `∀ x ∈ S, (f x, g x) ∈ V`. -/
+protected def gen (S : set α) (V : set (β × β)) : set ((α → β) × (α → β)) :=
+  {uv : (α → β) × (α → β) | ∀ x ∈ S, (uv.1 x, uv.2 x) ∈ V}
+
+/-- For `S : set α` and `V : set (β × β)`, we have
+`uniform_convergence_on.gen S V = (S.restrict × S.restrict) ⁻¹' (uniform_convergence.gen S β V)`.
+This is the crucial fact for proving that the family `uniform_convergence_on.gen S V` for
+`S ∈ 𝔖` and `V ∈ 𝓤 β` is indeed a basis for the uniformity `α → β` endowed with `𝒱(α, β, 𝔖, uβ)`
+the uniform structure of `𝔖`-convergence, as defined in `uniform_convergence_on.uniform_space`. -/
+protected lemma gen_eq_preimage_restrict (S : set α) (V : set (β × β)) :
+  uniform_convergence_on.gen S V =
+  (prod.map S.restrict S.restrict) ⁻¹' (uniform_convergence.gen S β V) :=
+begin
+  ext uv,
+  exact ⟨λ h ⟨x, hx⟩, h x hx, λ h x hx, h ⟨x, hx⟩⟩
+end
+
+/-- `uniform_convergence_on.gen` is antitone in the first argument and monotone in the second. -/
+protected lemma gen_mono {S S' : set α} {V V' : set (β × β)} (hS : S' ⊆ S) (hV : V ⊆ V') :
+  uniform_convergence_on.gen S V ⊆ uniform_convergence_on.gen S' V' :=
+λ uv h x hx, hV (h x $ hS hx)
+
+/-- If `𝔖 : set (set α)` is nonempty and directed and `𝓑` is a filter basis on `β × β`, then the
+family `uniform_convergence_on.gen S V` for `S ∈ 𝔖` and `V ∈ 𝓑` is a filter basis.
+We will show in `has_basis_uniformity_of_basis` that, if `𝓑` is a basis for `𝓤 β`, then the
+corresponding filter is the uniformity of `(α → β, 𝒱(α, β, 𝔖, uβ))`. -/
+protected lemma is_basis_gen (𝔖 : set (set α)) (h : 𝔖.nonempty) (h' : directed_on (⊆) 𝔖)
+  (𝓑 : filter_basis $ β × β) :
+  is_basis (λ SV : set α × set (β × β), SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓑)
+    (λ SV, uniform_convergence_on.gen SV.1 SV.2) :=
+⟨h.prod 𝓑.nonempty, λ U₁V₁ U₂V₂ h₁ h₂,
+  let ⟨U₃, hU₃, hU₁₃, hU₂₃⟩ := h' U₁V₁.1 h₁.1 U₂V₂.1 h₂.1 in
+  let ⟨V₃, hV₃, hV₁₂₃⟩ := 𝓑.inter_sets h₁.2 h₂.2 in ⟨⟨U₃, V₃⟩, ⟨⟨hU₃, hV₃⟩, λ uv huv,
+    ⟨(λ x hx, (hV₁₂₃ $ huv x $ hU₁₃ hx).1), (λ x hx, (hV₁₂₃ $ huv x $ hU₂₃ hx).2)⟩⟩⟩⟩
+
+variables (α β) [uniform_space β] (𝔖 : set (set α))
+
 /-- Uniform structure of `𝔖`-convergence, i.e uniform convergence on the elements of `𝔖`.
 It is defined as the infimum, for `S ∈ 𝔖`, of the pullback of `𝒰 S β` by `S.restrict`, the
 map of restriction to `S`. We will denote it `𝒱(α, β, 𝔖, uβ)`, where `uβ` is the uniform structure
@@ -499,6 +553,70 @@ begin
   refl
 end
 
+protected lemma has_basis_uniformity_of_basis_aux₁ {p : ι → Prop} {s : ι → set (β × β)}
+  (hb : has_basis (𝓤 β) p s) (S : set α) :
+  (@uniformity (α → β) ((uniform_convergence.uniform_space S β).comap S.restrict)).has_basis
+  p (λ i, uniform_convergence_on.gen S (s i)) :=
+begin
+  simp_rw [uniform_convergence_on.gen_eq_preimage_restrict, uniformity_comap rfl],
+  exact (uniform_convergence.has_basis_uniformity_of_basis S β hb).comap _
+end
+
+protected lemma has_basis_uniformity_of_basis_aux₂ (h : directed_on (⊆) 𝔖) {p : ι → Prop}
+  {s : ι → set (β × β)} (hb : has_basis (𝓤 β) p s) :
+  directed_on ((λ s : set α, (uniform_convergence.uniform_space s β).comap
+    (s.restrict : (α → β) → s → β)) ⁻¹'o ge) 𝔖 :=
+h.mono $ λ s t hst,
+  ((uniform_convergence_on.has_basis_uniformity_of_basis_aux₁ α β hb _).le_basis_iff
+    (uniform_convergence_on.has_basis_uniformity_of_basis_aux₁ α β hb _)).mpr
+  (λ V hV, ⟨V, hV, uniform_convergence_on.gen_mono hst subset_rfl⟩)
+
+/-- If `𝔖 : set (set α)` is nonempty and directed and `𝓑` is a filter basis of `𝓤 β`, then the
+uniformity of `(α → β, 𝒱(α, β, 𝔖, uβ))` admits the family `{(f, g) | ∀ x ∈ S, (f x, g x) ∈ V}` for
+`S ∈ 𝔖` and `V ∈ 𝓑` as a filter basis. -/
+protected lemma has_basis_uniformity_of_basis (h : 𝔖.nonempty) (h' : directed_on (⊆) 𝔖)
+  {p : ι → Prop} {s : ι → set (β × β)} (hb : has_basis (𝓤 β) p s) :
+  (@uniformity (α → β) (uniform_convergence_on.uniform_space α β 𝔖)).has_basis
+    (λ Si : set α × ι, Si.1 ∈ 𝔖 ∧ p Si.2)
+    (λ Si, uniform_convergence_on.gen Si.1 (s Si.2)) :=
+begin
+  simp only [infi_uniformity'],
+  exact has_basis_binfi_of_directed h (λ S, (@uniform_convergence_on.gen α β S) ∘ s) _
+    (λ S hS, uniform_convergence_on.has_basis_uniformity_of_basis_aux₁ α β hb S)
+    (uniform_convergence_on.has_basis_uniformity_of_basis_aux₂ α β 𝔖 h' hb)
+end
+
+/-- If `𝔖 : set (set α)` is nonempty and directed, then the uniformity of
+`(α → β, 𝒱(α, β, 𝔖, uβ))` admits the family `{(f, g) | ∀ x ∈ S, (f x, g x) ∈ V}` for `S ∈ 𝔖` and
+`V ∈ 𝓤 β` as a filter basis. -/
+protected lemma has_basis_uniformity (h : 𝔖.nonempty) (h' : directed_on (⊆) 𝔖) :
+  (@uniformity (α → β) (uniform_convergence_on.uniform_space α β 𝔖)).has_basis
+    (λ SV : set α × set (β × β), SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓤 β)
+    (λ SV, uniform_convergence_on.gen SV.1 SV.2) :=
+uniform_convergence_on.has_basis_uniformity_of_basis α β 𝔖 h h' (𝓤 β).basis_sets
+
+/-- If `α → β` is endowed with the topology of `𝔖`-convergence, where `𝔖 : set (set α)` is
+nonempty and directed, then `𝓝 f` admits the family `{g | ∀ x ∈ S, (f x, g x) ∈ V}` for `S ∈ 𝔖`
+and `V ∈ 𝓑` as a filter basis, for any basis `𝓑` of `𝓤 β`. -/
+protected lemma has_basis_nhds_of_basis (f) (h : 𝔖.nonempty) (h' : directed_on (⊆) 𝔖)
+  {p : ι → Prop} {s : ι → set (β × β)} (hb : has_basis (𝓤 β) p s) :
+  (@nhds (α → β) (uniform_convergence_on.topological_space α β 𝔖) f).has_basis
+    (λ Si : set α × ι, Si.1 ∈ 𝔖 ∧ p Si.2)
+    (λ Si, {g | (g, f) ∈ uniform_convergence_on.gen Si.1 (s Si.2)}) :=
+begin
+  letI : uniform_space (α → β) := uniform_convergence_on.uniform_space α β 𝔖,
+  exact nhds_basis_uniformity (uniform_convergence_on.has_basis_uniformity_of_basis α β 𝔖 h h' hb)
+end
+
+/-- If `α → β` is endowed with the topology of `𝔖`-convergence, where `𝔖 : set (set α)` is
+nonempty and directed, then `𝓝 f` admits the family `{g | ∀ x ∈ S, (f x, g x) ∈ V}` for `S ∈ 𝔖`
+and `V ∈ 𝓤 β` as a filter basis. -/
+protected lemma has_basis_nhds (f) (h : 𝔖.nonempty) (h' : directed_on (⊆) 𝔖) :
+  (@nhds (α → β) (uniform_convergence_on.topological_space α β 𝔖) f).has_basis
+    (λ SV : set α × set (β × β), SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓤 β)
+    (λ SV, {g | (g, f) ∈ uniform_convergence_on.gen SV.1 SV.2}) :=
+uniform_convergence_on.has_basis_nhds_of_basis α β 𝔖 f h h' (filter.basis_sets _)
+
 /-- If `S ∈ 𝔖`, then the restriction to `S` is a uniformly continuous map from `𝒱(α, β, 𝔖, uβ)` to
 `𝒰(↥S, β, uβ)`. -/
 protected lemma uniform_continuous_restrict (h : s ∈ 𝔖) :