OAI/Analysis/StrictMeans/TransportTest.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.StrictInverseFirstPower.transportTestline 11 - lemma
OAI.StrictInverseFirstPower.measurable_transportTestline 14 - lemma
OAI.StrictInverseFirstPower.transportTest_rebaseline 18 - lemma
OAI.StrictInverseFirstPower.truncatedPairingDomain_monoline 29 - lemma
OAI.StrictInverseFirstPower.mem_truncatedPairingDomain_eventuallyline 35 - lemma
OAI.StrictInverseFirstPower.transportTest_nat_monotoneline 50 - lemma
OAI.StrictInverseFirstPower.iSup_transportTestline 57