OAI/Analysis/JiangSu/CuntzSemigroup/RationalTerms.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.RationalTerms.Term line 11
  2. def OAI.RationalTerms.Term.eval line 21
  3. lemma OAI.RationalTerms.Term.map_eval line 28
  4. def OAI.RationalTerms.evalRange line 37
  5. lemma OAI.RationalTerms.evalRange_eq_adjoin line 45
  6. def OAI.RationalTerms.Term.sub line 63
  7. lemma OAI.RationalTerms.Term.eval_sub line 64
  8. lemma OAI.RationalTerms.eval_eq_of_norm line 68
  9. def OAI.RationalTerms.liftedValue line 72
  10. lemma OAI.RationalTerms.liftedValue_eq line 73
  11. def OAI.RationalTerms.lift line 75
  12. lemma OAI.RationalTerms.lift_norm line 94
  13. def OAI.RationalTerms.Term.boundedEval line 109
  14. lemma OAI.RationalTerms.Term.boundedEval_apply line 115
  15. lemma OAI.RationalTerms.Term.mk_boundedEval line 123
  16. def OAI.RationalTerms.Term.support line 134
  17. lemma OAI.RationalTerms.Term.eval_agree line 140