OAI/Analysis/Pureness/Operators/CStarHomClosedRange.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.starHomClosedKernel line 12
2. lemma OAI.CuntzPureness.starHomClosedKernel_mem line 26
3. lemma OAI.CuntzPureness.ClosedStarIdeal.liftStarHom_rel line 34
4. def OAI.CuntzPureness.ClosedStarIdeal.liftStarHom line 41
5. lemma OAI.CuntzPureness.ClosedStarIdeal.liftStarHom_map line 48
6. lemma OAI.CuntzPureness.ClosedStarIdeal.liftStarHom_injective line 51
7. lemma OAI.CuntzPureness.ClosedStarIdeal.liftStarHom_range line 63
8. theorem OAI.CuntzPureness.starHom_isClosed_range line 75
9. theorem OAI.CuntzPureness.starHom_surjective_of_denseRange line 82
10. theorem OAI.CuntzPureness.starHom_exists_lift_norm_lt line 89