OAI/Analysis/LipschitzEquivalence/SmoothRows.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzCounterexample.CompactWSC.molPair line 21
2. def OAI.LipschitzCounterexample.CompactWSC.smoothPair line 26
3. theorem OAI.LipschitzCounterexample.CompactWSC.smoothPair_apply line 28
4. theorem OAI.LipschitzCounterexample.CompactWSC.dual_molecular line 32
5. theorem OAI.LipschitzCounterexample.CompactWSC.test_molecular line 37
6. theorem OAI.LipschitzCounterexample.CompactWSC.molPair_approx line 48
7. theorem OAI.LipschitzCounterexample.CompactWSC.finite_smooth_pair_approx line 70
8. structure OAI.LipschitzCounterexample.CompactWSC.RowItem line 96
9. def OAI.LipschitzCounterexample.CompactWSC.triangularRows line 105
10. theorem OAI.LipschitzCounterexample.CompactWSC.triangularRows_rich line 112