OAI/Analysis/Commutator/FreeSequenceUnitary.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.TracialSequence.sequenceUnitary_free line 27
2. def OAI.Kadison.TracialSequence.restrictBoundedUnitary line 63
3. lemma OAI.Kadison.TracialSequence.map_restrictBoundedUnitary line 67
4. lemma OAI.Kadison.TracialSequence.sequenceUnitary_in_relative_range line 72
5. lemma OAI.Kadison.TracialSequence.constant_in_relative_range line 80