OAI/Analysis/BiholderTransport/Contact/GraphCompact.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakMTWTransport.isClosed_subgradientGraphline 247 - lemma
OAI.WeakMTWTransport.isCompact_subgradientGraphline 313