OAI/Analysis/WeakInfiniteness/UnitaryIntertwining.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.unitizationInnerFun line 27
2. lemma OAI.WeakPureInfiniteness.inr_unitizationInnerFun line 30
3. def OAI.WeakPureInfiniteness.unitizationInnerHom line 37
4. lemma OAI.WeakPureInfiniteness.unitizationInnerFun_star_left line 56
5. def OAI.WeakPureInfiniteness.unitizationInnerEquiv line 62
6. def OAI.WeakPureInfiniteness.UnitaryFiniteIntertwining line 69
7. lemma OAI.WeakPureInfiniteness.UnitaryFiniteIntertwining.finiteIntertwining line 75