OAI/Analysis/LipschitzEquivalence/FiniteReduction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LipschitzCounterexample.FreeSpace.Near line 20
  2. theorem OAI.LipschitzCounterexample.FreeSpace.near_mono line 24
  3. theorem OAI.LipschitzCounterexample.FreeSpace.subset_near line 29
  4. theorem OAI.LipschitzCounterexample.FreeSpace.prefix_finite_approx line 33
  5. theorem OAI.LipschitzCounterexample.FreeSpace.cutoff_product_bound line 48
  6. theorem OAI.LipschitzCounterexample.FreeSpace.finite_escape_step line 60
  7. theorem OAI.LipschitzCounterexample.FreeSpace.uniform_finite_neighborhood_approx line 140