OAI/Analysis/BiholderTransport/Regularity/SampleCenterFamilies.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakMTWTransport.WeakMTW.coordinateBackward_graph_poleline 22 - def
OAI.WeakMTWTransport.WeakMTW.center_sequence_of_graphline 36