OAI/Analysis/Pureness/Cuntz/SemigroupStateBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.OrderedSemigroup.restrictState line 12
2. theorem OAI.CuntzPureness.OrderedSemigroup.restrict_extendState line 16
3. theorem OAI.CuntzPureness.OrderedSemigroup.nonempty_states_iff_principalIdeal line 23
4. theorem OAI.CuntzPureness.OrderedSemigroup.state_gap_iff_principalIdeal line 28
5. theorem OAI.CuntzPureness.OrderedSemigroup.uniform_state_gap line 39
6. def OAI.CuntzPureness.OrderedSemigroup.stateRealOnIdeal line 50
7. theorem OAI.CuntzPureness.OrderedSemigroup.stateRealOnIdeal_monotone line 59
8. theorem OAI.CuntzPureness.OrderedSemigroup.stateRealOnIdeal_unit line 64
9. theorem OAI.CuntzPureness.OrderedSemigroup.no_state_of_properlyInfinite line 70