OAI/Analysis/StrictMeans/CriticalRanks.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.signedCriticalFiber line 11
  2. def OAI.StrictInverseFirstPower.criticalRank line 16
  3. lemma OAI.StrictInverseFirstPower.signedCriticalFiber_strictCut_finite line 20
  4. lemma OAI.StrictInverseFirstPower.goodPair_criticalHeight_injOn line 29
  5. lemma OAI.StrictInverseFirstPower.criticalRank_injOn line 36
  6. abbrev OAI.StrictInverseFirstPower.RankParameters line 44
  7. def OAI.StrictInverseFirstPower.rankClosedRelation line 46
  8. def OAI.StrictInverseFirstPower.rankOpenRelation line 49
  9. lemma OAI.StrictInverseFirstPower.continuous_rank_f line 55
  10. lemma OAI.StrictInverseFirstPower.continuous_rank_z line 59
  11. lemma OAI.StrictInverseFirstPower.isClosed_rankClosedRelation line 63
  12. lemma OAI.StrictInverseFirstPower.isOpen_rankOpenRelation line 69
  13. lemma OAI.StrictInverseFirstPower.rankRelation_finite line 81
  14. lemma OAI.StrictInverseFirstPower.measurable_criticalRank line 88