OAI/Analysis/JiangSu/CuntzSemigroup/FiniteCuntzFullness.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Pureness.finitePositiveClass_eq_zero_iff line 16
2. theorem OAI.Pureness.positive_le_norm_smul_one line 27
3. theorem OAI.Pureness.finitePositiveClass_dominated line 31
4. theorem OAI.Pureness.finiteCuntz_nonzero_orderUnit line 60
5. theorem OAI.Pureness.finiteCuntz_state_finite line 79