OAI/Analysis/CStarAlgebra/PureInfiniteness/PositiveFunctional.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MainGap.norm_add_one_of_nonneg line 13
2. lemma OAI.MainGap.real_norm_one_positive line 23
3. def OAI.MainGap.realPartCLM line 38
4. lemma OAI.MainGap.realPartCLM_apply line 45
5. lemma OAI.MainGap.norm_realPartCLM line 48
6. lemma OAI.MainGap.exists_norming_positive line 53