OAI/Analysis/BiholderTransport/Coordinates/CutCharacterization.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakMTWTransport.joint_exp_locally_injective_of_nonconjugateline 20 - lemma
OAI.WeakMTWTransport.mem_injectivityDomain_of_nonconjugate_uniqueline 32