add direct IsContinuousLinearMap rule for FunLike.coe

- this is necessary as there are some odd issues with product topology(likely a bug)
lecopivo · Jul 27, 2023 · 915a4b4 · 915a4b4
1 parent 33276f7
commit 915a4b4
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/SciLean/FunctionSpaces/ContinuousLinearMap/Basic.lean b/SciLean/FunctionSpaces/ContinuousLinearMap/Basic.lean
@@ -234,6 +234,15 @@ variable
 -- FunLike.coe -----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
+-- This one is necessary because of some issues with topology on product spaces
+-- This problem has to be a bug somewhere ...
+@[fprop_rule]
+theorem FunLike.coe.arg_f.IsContinuousLinearMap
+  (f : Y →L[R] Z) 
+  : SciLean.IsContinuousLinearMap R f := 
+  by_morphism f (by simp)
+
+
 @[fprop_rule]
 theorem FunLike.coe.arg_f.IsContinuousLinearMap_comp  
   (f : Y →L[R] Z) (g : X → Y) (hg : SciLean.IsContinuousLinearMap R g)