OAI/Analysis/JiangSu/TensorProducts/FaithfulTensorExtension.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Pureness.tensorRangeClosure line 18
2. instance OAI.Pureness.tensorRangeClosure_closed line 19
3. instance OAI.Pureness.(instance at line 21) line 21
4. def OAI.Pureness.tensorRangeMap line 23
5. lemma OAI.Pureness.tensorRangeMap_injective line 25
6. lemma OAI.Pureness.tensorRangeMap_dense line 27
7. def OAI.Pureness.faithfulTensorExtension line 38
8. lemma OAI.Pureness.faithfulTensorExtension_apply line 42