OAI/Analysis/Pureness/Completion/ClosedStarIdealQuotientCStar.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.ClosedStarIdeal.idealStarAlgebra line 11
2. instance OAI.CuntzPureness.ClosedStarIdeal.idealStarAlgebraCompleteSpace line 22
3. instance OAI.CuntzPureness.ClosedStarIdeal.idealStarAlgebraCStar line 24
4. instance OAI.CuntzPureness.ClosedStarIdeal.idealPartialOrder line 27
5. instance OAI.CuntzPureness.ClosedStarIdeal.idealStarOrderedRing line 29
6. def OAI.CuntzPureness.ClosedStarIdeal.idealInclusion line 35
7. lemma OAI.CuntzPureness.ClosedStarIdeal.idealInclusion_nonneg line 43
8. lemma OAI.CuntzPureness.ClosedStarIdeal.norm_one_sub line 52
9. lemma OAI.CuntzPureness.ClosedStarIdeal.exists_ideal_contraction line 59
10. lemma OAI.CuntzPureness.ClosedStarIdeal.quotient_norm_square_le line 76
11. instance OAI.CuntzPureness.ClosedStarIdeal.quotientCStarAlgebra line 117