OAI/Analysis/StrictMeans/RegularLevels.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.StrictInverseFirstPower.goodPair_lower_regular_cutline 11 - lemma
OAI.StrictInverseFirstPower.source_squared_critical_strictline 39 - lemma
OAI.StrictInverseFirstPower.source_squared_interiorline 53 - lemma
OAI.StrictInverseFirstPower.source_poles_subsingletonline 62