OAI/Analysis/Pureness/Cuntz/SemigroupGrothendieck.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CuntzPureness.OrderedSemigroup.grothendieck_eq_iff line 11
2. theorem OAI.CuntzPureness.OrderedSemigroup.grothendieck_difference_eq_iff line 18
3. theorem OAI.CuntzPureness.OrderedSemigroup.grothendieck_exists_difference line 24
4. def OAI.CuntzPureness.OrderedSemigroup.grothendieckCone line 35
5. theorem OAI.CuntzPureness.OrderedSemigroup.grothendieck_mem_cone_iff line 42
6. lemma OAI.CuntzPureness.OrderedSemigroup.grothendieck_of_nonneg line 57
7. theorem OAI.CuntzPureness.OrderedSemigroup.grothendieck_orderUnit line 61