Finished

src/topology/uniform_space/uniform_convergence_topology.lean

@@ -12,7 +12,7 @@ import topology.uniform_space.pi
 This files endows `α → β` with the topologies / uniform structures of
 - uniform convergence on `α` (in the `uniform_convergence` namespace)
 - uniform convergence on a specified family `𝔖` of sets of `α`
-  (in the `uniform_convergence_on` namespace)
+  (in the `uniform_convergence_on` namespace), also called `𝔖`-convergence
 
 Usual examples of the second construction include :
 - the topology of compact convergence, when `𝔖` is the set of compacts of `α`
@@ -22,19 +22,34 @@ Usual examples of the second construction include :
 
 ## Main definitions
 
-* `foo_bar`
+* `uniform_convergence.gen` : basis sets for the uniformity of uniform convergence
+* `uniform_convergence.uniform_space` : uniform structure of uniform convergence
+* `uniform_convergence_on.uniform_space` : uniform structure of 𝔖-convergence
 
 ## Main statements
 
-* `foo_bar_unique`
-
-## Notation
-
+* `uniform_convergence.uniform_continuous_eval` : evaluation is uniformly continuous
+* `uniform_convergence.t2_space` : the topology of uniform convergence on `α → β` is T2 if
+  `β` is T2.
+* `uniform_convergence.tendsto_iff_tendsto_uniformly` : `uniform_convergence.uniform_space` is
+  indeed the uniform structure of uniform convergence
 
+* `uniform_convergence_on.uniform_continuous_eval_of_mem` : evaluation at a point contained in a
+  set of `𝔖` is uniformly continuous
+* `uniform_convergence.t2_space` : the topology of `𝔖`-convergence on `α → β` is T2 if
+  `β` is T2 and `𝔖` covers `α`
+* `uniform_convergence_on.tendsto_iff_tendsto_uniformly_on` :
+  `uniform_convergence_on.uniform_space` is indeed the uniform structure of `𝔖`-convergence
 
 ## Implementation details
 
+We do not declare these structures as instances, since they would conflict with `Pi.uniform_space`.
+
+## TODO
 
+* Show that the uniform structure of `𝔖`-convergence is exactly the structure of `𝔖'`-convergence,
+  where `𝔖'` is the bornology generated by `𝔖`.
+* Add a type synonym for `α → β` endowed with the structures of uniform convergence
 
 ## References
 
@@ -58,6 +73,7 @@ namespace uniform_convergence
 variables (α β : Type*) {γ ι : Type*} [uniform_space β]
 variables {F : ι → α → β} {f : α → β} {s s' : set α} {x : α} {p : filter ι} {g : ι → α}
 
+/-- Basis sets for the uniformity of uniform convergence -/
 protected def gen (V : set (β × β)) : set ((α → β) × (α → β)) :=
   {uv : (α → β) × (α → β) | ∀ x, (uv.1 x, uv.2 x) ∈ V}
 
@@ -66,9 +82,11 @@ protected lemma is_basis_gen :
 ⟨⟨univ, univ_mem⟩, λ U V hU hV, ⟨U ∩ V, inter_mem hU hV, λ uv huv,
   ⟨λ x, (huv x).left, λ x, (huv x).right⟩⟩⟩
 
+/-- Filter basis for the uniformity of uniform convergence -/
 protected def uniformity_basis : filter_basis ((α → β) × (α → β)) :=
 (uniform_convergence.is_basis_gen α β).filter_basis
 
+/-- Core of the uniform structure of uniform convergence -/
 protected def uniform_core : uniform_space.core (α → β) :=
 uniform_space.core.mk_of_basis (uniform_convergence.uniformity_basis α β)
   (λ U ⟨V, hV, hVU⟩ f, hVU ▸ λ x, refl_mem_uniformity hV)
@@ -78,6 +96,7 @@ uniform_space.core.mk_of_basis (uniform_convergence.uniformity_basis α β)
     ⟨uniform_convergence.gen α β W, ⟨W, hW, rfl⟩, λ uv ⟨w, huw, hwv⟩ x, hWV
       ⟨w x, by exact ⟨huw x, hwv x⟩⟩⟩)
 
+/-- Uniform structure of uniform convergence -/
 protected def uniform_space : uniform_space (α → β) :=
 uniform_space.of_core (uniform_convergence.uniform_core α β)
 
@@ -86,6 +105,7 @@ protected lemma has_basis_uniformity :
   (uniform_convergence.gen α β) :=
 (uniform_convergence.is_basis_gen α β).has_basis
 
+/-- Topology of uniform convergence -/
 protected def topological_space : topological_space (α → β) :=
 (uniform_convergence.uniform_space α β).to_topological_space
 
@@ -148,10 +168,12 @@ namespace uniform_convergence_on
 variables (α β : Type*) {γ ι : Type*} [uniform_space β] (𝔖 : set (set α))
 variables {F : ι → α → β} {f : α → β} {s s' : set α} {x : α} {p : filter ι} {g : ι → α}
 
+/-- Uniform structure of uniform convergence on the sets of `𝔖`. -/
 protected def uniform_space : uniform_space (α → β) :=
 ⨅ (s : set α) (hs : s ∈ 𝔖), uniform_space.comap (λ f, s.restrict f)
   (uniform_convergence.uniform_space s β)
 
+/-- Topology of uniform convergence on the sets of `𝔖`. -/
 protected def topological_space : topological_space (α → β) :=
 (uniform_convergence_on.uniform_space α β 𝔖).to_topological_space