OAI/Analysis/JiangSu/TensorProducts/StarHomClosureExtension.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StarHomClosure.inclusion line 13
2. lemma OAI.StarHomClosure.inclusion_dense line 14
3. def OAI.StarHomClosure.extensionLinear line 17
4. lemma OAI.StarHomClosure.extensionLinear_eq line 20
5. def OAI.StarHomClosure.extension line 26
6. lemma OAI.StarHomClosure.extension_eq line 51
7. lemma OAI.StarHomClosure.extension_continuous line 53
8. lemma OAI.StarHomClosure.extension_norm line 54