OAI/Analysis/StrictMeans/TransportPairing.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.availableSource line 11
  2. lemma OAI.StrictInverseFirstPower.availableSource_injective line 14
  3. lemma OAI.StrictInverseFirstPower.measurable_availableSource line 26
  4. lemma OAI.StrictInverseFirstPower.measurableEmbedding_availableSource line 30
  5. def OAI.StrictInverseFirstPower.sourcePairingDomain line 35
  6. lemma OAI.StrictInverseFirstPower.measurableSet_sourcePairingDomain line 37
  7. def OAI.StrictInverseFirstPower.sourcePair line 40
  8. lemma OAI.StrictInverseFirstPower.sourcePair_apply line 42
  9. lemma OAI.StrictInverseFirstPower.measurable_sourcePair line 45
  10. def OAI.StrictInverseFirstPower.sourcePartnerOn line 56
  11. lemma OAI.StrictInverseFirstPower.measurable_sourcePartnerOn line 59
  12. def OAI.StrictInverseFirstPower.sourcePartner line 62
  13. lemma OAI.StrictInverseFirstPower.sourcePartner_of_mem line 67
  14. lemma OAI.StrictInverseFirstPower.measurable_sourcePartner line 72
  15. lemma OAI.StrictInverseFirstPower.sourcePairingDomain_iff line 76
  16. lemma OAI.StrictInverseFirstPower.sourcePartner_spec line 98
  17. lemma OAI.StrictInverseFirstPower.sourcePartner_injOn_fiber line 123