OAI/Analysis/LipschitzEquivalence/CompactReduction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.LipschitzCounterexample.FreeSpace.LocalizationState line 20
2. theorem OAI.LipschitzCounterexample.FreeSpace.localization_step line 29
3. theorem OAI.LipschitzCounterexample.FreeSpace.bounded_compact_reduction line 60
4. theorem OAI.LipschitzCounterexample.FreeSpace.hasCompactReduction line 116