From 915a4b46c4c65e3299fd2ec70dfde7b21c53303a Mon Sep 17 00:00:00 2001 From: lecopivo Date: Thu, 27 Jul 2023 12:49:28 -0400 Subject: [PATCH] add direct IsContinuousLinearMap rule for FunLike.coe - this is necessary as there are some odd issues with product topology(likely a bug) --- SciLean/FunctionSpaces/ContinuousLinearMap/Basic.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/SciLean/FunctionSpaces/ContinuousLinearMap/Basic.lean b/SciLean/FunctionSpaces/ContinuousLinearMap/Basic.lean index 6ec5b30e..5b7b3fa7 100644 --- 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)