OAI/Analysis/BiholderTransport/Coordinates/TotalInjectivity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.joint_exp_locally_injective line 98
2. lemma OAI.WeakMTWTransport.interior_total_minimizingVectors line 120
3. lemma OAI.WeakMTWTransport.total_injectivityDomain_eq_interior line 137
4. lemma OAI.WeakMTWTransport.isOpen_total_injectivityDomain line 149
5. lemma OAI.WeakMTWTransport.contMDiff_tangent_energy line 164