OAI/Analysis/JiangSu/Nonunital/NormMaps.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.NonunitalNormMaps.boundedMap line 16
2. lemma OAI.NonunitalNormMaps.boundedMap_apply line 27
3. lemma OAI.NonunitalNormMaps.boundedMap_constant line 31
4. def OAI.NonunitalNormMaps.quotientMap line 34
5. lemma OAI.NonunitalNormMaps.quotientMap_mk line 65
6. lemma OAI.NonunitalNormMaps.quotientMap_inclusion line 68
7. lemma OAI.NonunitalNormMaps.quotientMap_commute line 73