OAI/Analysis/Pureness/States/FiniteFamilyMetric.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.positiveLevel line 16
2. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.positiveLevel_block_add line 19
3. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.positive_square_root line 23
4. theorem OAI.CuntzPureness.CompatibleFiniteQuasitrace.positiveLevel_add_weighted line 27
5. theorem OAI.CuntzPureness.CompatibleFiniteQuasitrace.positiveLevel_sqrt_add line 68
6. theorem OAI.CuntzPureness.CompatibleFiniteQuasitrace.positiveLevel_metricSize_add line 76