OAI/Analysis/BiholderTransport/Regularity/FixedJoinUpper.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWTransport.movingFixedJoinAction line 43
2. def OAI.WeakMTWTransport.movingFixedJoinMiddle line 47
3. lemma OAI.WeakMTWTransport.movingFixedJoinAction_eq line 55
4. lemma OAI.WeakMTWTransport.movingFixedJoinAction_contDiffAt line 67
5. lemma OAI.WeakMTWTransport.movingFixedJoinMiddle_contDiffAt line 123
6. lemma OAI.WeakMTWTransport.movingFixedJoinMiddle_eq line 134
7. lemma OAI.WeakMTWTransport.movingFixedJoinMiddle_trivialization line 162