OAI/Analysis/Pureness/Cuntz/SemigroupStates.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.OrderedSemigroup.IsNormalizedState line 12
  2. abbrev OAI.CuntzPureness.OrderedSemigroup.StateSpace line 15
  3. def OAI.CuntzPureness.OrderedSemigroup.StateSpace.toAddHom line 19
  4. lemma OAI.CuntzPureness.OrderedSemigroup.StateSpace.monotone line 24
  5. lemma OAI.CuntzPureness.OrderedSemigroup.StateSpace.at_unit line 25
  6. lemma OAI.CuntzPureness.OrderedSemigroup.StateSpace.at_zero line 26
  7. lemma OAI.CuntzPureness.OrderedSemigroup.StateSpace.at_add line 27
  8. lemma OAI.CuntzPureness.OrderedSemigroup.StateSpace.at_nsmul line 28
  9. lemma OAI.CuntzPureness.OrderedSemigroup.StateSpace.continuous_eval line 31
  10. lemma OAI.CuntzPureness.OrderedSemigroup.isClosed_normalizedStates line 35
  11. instance OAI.CuntzPureness.OrderedSemigroup.compactSpace_states line 49
  12. def OAI.CuntzPureness.OrderedSemigroup.principalIdeal line 54
  13. lemma OAI.CuntzPureness.OrderedSemigroup.mem_principalIdeal line 61
  14. lemma OAI.CuntzPureness.OrderedSemigroup.principalIdeal_downward line 62
  15. lemma OAI.CuntzPureness.OrderedSemigroup.add_mem_principalIdeal_iff line 67
  16. theorem OAI.CuntzPureness.OrderedSemigroup.state_finite_on_principalIdeal line 75
  17. def OAI.CuntzPureness.OrderedSemigroup.extendState line 82
  18. lemma OAI.CuntzPureness.OrderedSemigroup.extendState_apply line 109