OAI/Analysis/WeakInfiniteness/UnitalCuntzEmbedding.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.spectralRamp_one line 32
2. lemma OAI.WeakPureInfiniteness.exists_two_isometries_of_properlyInfinite line 39
3. lemma OAI.WeakPureInfiniteness.star_pow_mul_pow_of_isometry line 48
4. lemma OAI.WeakPureInfiniteness.star_mul_power_of_orthogonal line 59
5. lemma OAI.WeakPureInfiniteness.binaryCuntzFamily_relations line 65
6. lemma OAI.WeakPureInfiniteness.norm_commutator_of_cuntz_isometries line 93
7. theorem OAI.WeakPureInfiniteness.exists_oInfinityHom_of_exact_weaklyPurelyInfinite line 114