OAI/Analysis/JiangSu/CuntzSemigroup/RationalConeStates.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Pureness.RationalRiesz.exists_normalized_positive line 17
  2. def OAI.Pureness.RationalRiesz.adjoinNegative line 43
  3. lemma OAI.Pureness.RationalRiesz.mem_adjoinNegative line 53
  4. theorem OAI.Pureness.RationalRiesz.separating_state line 56
  5. theorem OAI.Pureness.RationalRiesz.strict_bound_of_states line 95
  6. lemma OAI.Pureness.OrderedSemigroup.rational_nat_mul line 111
  7. def OAI.Pureness.OrderedSemigroup.rationalCone line 121
  8. lemma OAI.Pureness.OrderedSemigroup.rationalCone_of_mem line 142
  9. theorem OAI.Pureness.OrderedSemigroup.rationalCone_of_iff line 145
  10. theorem OAI.Pureness.OrderedSemigroup.rationalCone_orderUnit line 157
  11. abbrev OAI.Pureness.OrderedSemigroup.semigroupRationalMap line 182
  12. abbrev OAI.Pureness.OrderedSemigroup.semigroupRationalCone line 185
  13. def OAI.Pureness.OrderedSemigroup.stateOfRationalPositive line 188
  14. theorem OAI.Pureness.OrderedSemigroup.exists_strict_buffer_of_states line 208
  15. theorem OAI.Pureness.OrderedSemigroup.le_of_states line 259