OAI/Analysis/Pureness/Projections/PartialIsometryMatch.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CuntzPureness.ProjectionMatch line 8
2. theorem OAI.CuntzPureness.ProjectionMatch.ext line 19
3. instance OAI.CuntzPureness.ProjectionMatch.projectionMatchPartialOrder line 22
4. lemma OAI.CuntzPureness.ProjectionMatch.le_def line 38
5. def OAI.CuntzPureness.ProjectionMatch.zero line 41
6. lemma OAI.CuntzPureness.ProjectionMatch.zero_le line 48
7. theorem OAI.CuntzPureness.ProjectionMatch.exists_extension line 53