OAI/Analysis/StrictMeans/RankPairing.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.StrictInverseFirstPower.diskFamily_standardBorel line 11
  2. instance OAI.StrictInverseFirstPower.rankParameters_standardBorel line 15
  3. def OAI.StrictInverseFirstPower.RankPairRelation line 18
  4. lemma OAI.StrictInverseFirstPower.measurableSet_rankPairRelation line 25
  5. lemma OAI.StrictInverseFirstPower.rankPairRelation_unique line 54
  6. def OAI.StrictInverseFirstPower.rankPairingDomain line 58
  7. lemma OAI.StrictInverseFirstPower.measurableSet_rankPairingDomain line 61
  8. abbrev OAI.StrictInverseFirstPower.AvailableRankPair line 87
  9. def OAI.StrictInverseFirstPower.availableRankPartner line 89
  10. lemma OAI.StrictInverseFirstPower.availableRankPartner_spec line 92
  11. lemma OAI.StrictInverseFirstPower.measurable_availableRankPartner line 95
  12. lemma OAI.StrictInverseFirstPower.availableRankPartner_injOn_fiber line 114