OAI/Analysis/JiangSu/CuntzSemigroup/SemigroupStates.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Pureness.OrderedSemigroup.IsNormalizedState line 13
2. abbrev OAI.Pureness.OrderedSemigroup.StateSpace line 16
3. def OAI.Pureness.OrderedSemigroup.StateSpace.toAddHom line 20
4. lemma OAI.Pureness.OrderedSemigroup.StateSpace.monotone line 25
5. lemma OAI.Pureness.OrderedSemigroup.StateSpace.at_unit line 26
6. lemma OAI.Pureness.OrderedSemigroup.StateSpace.at_zero line 27
7. lemma OAI.Pureness.OrderedSemigroup.StateSpace.at_add line 28
8. lemma OAI.Pureness.OrderedSemigroup.StateSpace.at_nsmul line 29
9. lemma OAI.Pureness.OrderedSemigroup.StateSpace.continuous_eval line 32
10. lemma OAI.Pureness.OrderedSemigroup.isClosed_normalizedStates line 36
11. instance OAI.Pureness.OrderedSemigroup.compactSpace_states line 50
12. def OAI.Pureness.OrderedSemigroup.principalIdeal line 55
13. lemma OAI.Pureness.OrderedSemigroup.mem_principalIdeal line 62
14. lemma OAI.Pureness.OrderedSemigroup.principalIdeal_downward line 63
15. lemma OAI.Pureness.OrderedSemigroup.add_mem_principalIdeal_iff line 68
16. theorem OAI.Pureness.OrderedSemigroup.state_finite_on_principalIdeal line 76
17. def OAI.Pureness.OrderedSemigroup.extendState line 83
18. lemma OAI.Pureness.OrderedSemigroup.extendState_apply line 110
19. def OAI.Pureness.OrderedSemigroup.restrictState line 122
20. theorem OAI.Pureness.OrderedSemigroup.restrict_extendState line 126
21. theorem OAI.Pureness.OrderedSemigroup.nonempty_states_iff_principalIdeal line 133
22. theorem OAI.Pureness.OrderedSemigroup.state_gap_iff_principalIdeal line 138
23. theorem OAI.Pureness.OrderedSemigroup.uniform_state_gap line 149
24. def OAI.Pureness.OrderedSemigroup.stateRealOnIdeal line 161
25. theorem OAI.Pureness.OrderedSemigroup.stateRealOnIdeal_monotone line 170
26. theorem OAI.Pureness.OrderedSemigroup.stateRealOnIdeal_unit line 175
27. theorem OAI.Pureness.OrderedSemigroup.no_state_of_properlyInfinite line 181