OAI/Analysis/Pureness/Stabilization/ZeroIdeal.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.CuntzTrace.lowerSemicontinuous_idealIndicatorline 8 - def
OAI.CuntzTrace.zeroIdealWeightline 25 - theorem
OAI.CuntzTrace.zeroIdealWeight_eq_zeroline 52 - theorem
OAI.CuntzTrace.zeroIdealWeight_lt_topline 56 - theorem
OAI.CuntzTrace.zeroIdealWeight_detectsline 62