OAI/Analysis/JiangSu/CStarAlgebras/StarTermsNormLift.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StarTerms.Term.sub line 13
2. lemma OAI.StarTerms.Term.eval_sub line 14
3. lemma OAI.StarTerms.eval_eq_of_norm line 18
4. def OAI.StarTerms.liftedValue line 22
5. lemma OAI.StarTerms.liftedValue_eq line 23
6. def OAI.StarTerms.lift line 25
7. lemma OAI.StarTerms.lift_norm line 44
8. def OAI.StarTerms.closureLift line 49
9. lemma OAI.StarTerms.closureLift_eval line 51
10. lemma OAI.StarTerms.closureLift_gen line 56