feat(Topology/Algebra/Module/StrongTopology): add monotonicity lemmas (#11600)

Author: mcdoll

Mathlib/Topology/Algebra/Module/StrongTopology.lean

@@ -83,15 +83,23 @@ instance instFunLike [TopologicalSpace F] [TopologicalAddGroup F]
     (𝔖 : Set (Set E)) : FunLike (UniformConvergenceCLM σ F 𝔖) E F :=
   ContinuousLinearMap.funLike
 
-instance continuousSemilinearMapClass [TopologicalSpace F] [TopologicalAddGroup F]
+instance instContinuousSemilinearMapClass [TopologicalSpace F] [TopologicalAddGroup F]
     (𝔖 : Set (Set E)) : ContinuousSemilinearMapClass (UniformConvergenceCLM σ F 𝔖) σ E F :=
   ContinuousLinearMap.continuousSemilinearMapClass
-instance instTopologicalSpace [TopologicalSpace F]
-    [TopologicalAddGroup F] (𝔖 : Set (Set E)) : TopologicalSpace (UniformConvergenceCLM σ F 𝔖) :=
+
+instance instTopologicalSpace [TopologicalSpace F] [TopologicalAddGroup F] (𝔖 : Set (Set E)) :
+    TopologicalSpace (UniformConvergenceCLM σ F 𝔖) :=
   (@UniformOnFun.topologicalSpace E F (TopologicalAddGroup.toUniformSpace F) 𝔖).induced
     (DFunLike.coe : (UniformConvergenceCLM σ F 𝔖) → (E →ᵤ[𝔖] F))
 #align continuous_linear_map.strong_topology UniformConvergenceCLM.instTopologicalSpace
 
+theorem topologicalSpace_eq [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) :
+    instTopologicalSpace σ F 𝔖 = TopologicalSpace.induced DFunLike.coe
+      (UniformOnFun.topologicalSpace E F 𝔖) := by
+  rw [instTopologicalSpace]
+  congr
+  exact UniformAddGroup.toUniformSpace_eq
+
 /-- The uniform structure associated with `ContinuousLinearMap.strongTopology`. We make sure
 that this has nice definitional properties. -/
 instance instUniformSpace [UniformSpace F] [UniformAddGroup F]
@@ -102,15 +110,18 @@ instance instUniformSpace [UniformSpace F] [UniformAddGroup F]
     (by rw [UniformConvergenceCLM.instTopologicalSpace, UniformAddGroup.toUniformSpace_eq]; rfl)
 #align continuous_linear_map.strong_uniformity UniformConvergenceCLM.instUniformSpace
 
+theorem uniformSpace_eq [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) :
+    instUniformSpace σ F 𝔖 = UniformSpace.comap DFunLike.coe (UniformOnFun.uniformSpace E F 𝔖) := by
+  rw [instUniformSpace, UniformSpace.replaceTopology_eq]
+
 @[simp]
 theorem uniformity_toTopologicalSpace_eq [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) :
     (UniformConvergenceCLM.instUniformSpace σ F 𝔖).toTopologicalSpace =
       UniformConvergenceCLM.instTopologicalSpace σ F 𝔖 :=
   rfl
 #align continuous_linear_map.strong_uniformity_topology_eq UniformConvergenceCLM.uniformity_toTopologicalSpace_eq
 
-theorem uniformEmbedding_coeFn [UniformSpace F] [UniformAddGroup F]
-    (𝔖 : Set (Set E)) :
+theorem uniformEmbedding_coeFn [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) :
     UniformEmbedding (α := UniformConvergenceCLM σ F 𝔖) (β := E →ᵤ[𝔖] F) DFunLike.coe :=
   ⟨⟨rfl⟩, DFunLike.coe_injective⟩
 #align continuous_linear_map.strong_uniformity.uniform_embedding_coe_fn UniformConvergenceCLM.uniformEmbedding_coeFn
@@ -208,6 +219,20 @@ theorem tendsto_iff_tendstoUniformlyOn {ι : Type*} {p : Filter ι} [UniformSpac
   rw [(embedding_coeFn σ F 𝔖).tendsto_nhds_iff, UniformOnFun.tendsto_iff_tendstoUniformlyOn]
   rfl
 
+variable {𝔖₁ 𝔖₂ : Set (Set E)}
+
+theorem uniformSpace_mono [UniformSpace F] [UniformAddGroup F] (h : 𝔖₂ ⊆ 𝔖₁) :
+    instUniformSpace σ F 𝔖₁ ≤ instUniformSpace σ F 𝔖₂ := by
+  simp_rw [uniformSpace_eq]
+  exact UniformSpace.comap_mono (UniformOnFun.mono (le_refl _) h)
+
+theorem topologicalSpace_mono [TopologicalSpace F] [TopologicalAddGroup F] (h : 𝔖₂ ⊆ 𝔖₁) :
+    instTopologicalSpace σ F 𝔖₁ ≤ instTopologicalSpace σ F 𝔖₂ := by
+  letI := TopologicalAddGroup.toUniformSpace F
+  haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
+  simp_rw [← uniformity_toTopologicalSpace_eq]
+  exact UniformSpace.toTopologicalSpace_mono (uniformSpace_mono σ F h)
+
 end UniformConvergenceCLM
 
 end General