OAI/Analysis/Pureness/Comparison/HereditaryApproximation.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CuntzComparison.supportCutoff_mul_errorline 9 - lemma
OAI.CuntzComparison.supportApprox_mul_self_errorline 22 - lemma
OAI.CuntzComparison.supportApprox_mul_self_tendstoline 33 - theorem
OAI.CuntzComparison.supportApprox_mul_tendstoline 40 - theorem
OAI.CuntzComparison.mul_supportApprox_tendstoline 69