OAI/Analysis/LipschitzEquivalence/SeparableCoordinates.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LipschitzCounterexample.CoordinateSpaces.Hilbert line 15
  2. def OAI.LipschitzCounterexample.CoordinateSpaces.coord line 17
  3. theorem OAI.LipschitzCounterexample.CoordinateSpaces.coord_apply line 21
  4. def OAI.LipschitzCounterexample.CoordinateSpaces.space line 23
  5. theorem OAI.LipschitzCounterexample.CoordinateSpaces.mem_space line 26
  6. theorem OAI.LipschitzCounterexample.CoordinateSpaces.space_isClosed line 30
  7. theorem OAI.LipschitzCounterexample.CoordinateSpaces.inner_eq_zero_of_disjoint line 34
  8. def OAI.LipschitzCounterexample.CoordinateSpaces.basisVector line 47
  9. theorem OAI.LipschitzCounterexample.CoordinateSpaces.basisVector_coord line 50
  10. theorem OAI.LipschitzCounterexample.CoordinateSpaces.basisVector_mem line 60
  11. theorem OAI.LipschitzCounterexample.CoordinateSpaces.space_eq_topologicalClosure_span line 67
  12. instance OAI.LipschitzCounterexample.CoordinateSpaces.(instance at line 111) line 111
  13. def OAI.LipschitzCounterexample.CoordinateSpaces.projection line 113
  14. theorem OAI.LipschitzCounterexample.CoordinateSpaces.projection_mem line 116
  15. theorem OAI.LipschitzCounterexample.CoordinateSpaces.norm_projection_le line 119
  16. theorem OAI.LipschitzCounterexample.CoordinateSpaces.inner_projection line 122
  17. theorem OAI.LipschitzCounterexample.CoordinateSpaces.norm_projection_sq line 127
  18. theorem OAI.LipschitzCounterexample.CoordinateSpaces.sum_projection_sq_le line 132
  19. theorem OAI.LipschitzCounterexample.HilbertSlots.cutHead_apply line 165
  20. theorem OAI.LipschitzCounterexample.HilbertSlots.tailCLM_coord line 173
  21. theorem OAI.LipschitzCounterexample.SeparatingStages.D_local_orthogonality line 186
  22. theorem OAI.LipschitzCounterexample.SeparatingStages.D_local_orthogonal_subspaces line 216
  23. def OAI.LipschitzCounterexample.FreeSpace.supported line 237
  24. theorem OAI.LipschitzCounterexample.FreeSpace.supported_isClosed line 240
  25. theorem OAI.LipschitzCounterexample.FreeSpace.point_mem_supported line 243
  26. theorem OAI.LipschitzCounterexample.FreeSpace.supported_le_ker line 246
  27. theorem OAI.LipschitzCounterexample.FreeSpace.supported_pairing_le line 253
  28. def OAI.LipschitzCounterexample.FreeSpace.HasCompactReduction line 271
  29. theorem OAI.LipschitzCounterexample.CoordinateSpaces.inner_basisVector_left line 281
  30. theorem OAI.LipschitzCounterexample.CoordinateSpaces.projection_coord line 286
  31. def OAI.LipschitzCounterexample.CoordinateSpaces.headSet line 294
  32. def OAI.LipschitzCounterexample.CoordinateSpaces.tailSet line 295
  33. def OAI.LipschitzCounterexample.CoordinateSpaces.head line 296
  34. def OAI.LipschitzCounterexample.CoordinateSpaces.tail line 297
  35. theorem OAI.LipschitzCounterexample.CoordinateSpaces.head_coord line 299
  36. theorem OAI.LipschitzCounterexample.CoordinateSpaces.tail_coord line 302
  37. theorem OAI.LipschitzCounterexample.CoordinateSpaces.head_add_tail line 306
  38. theorem OAI.LipschitzCounterexample.CoordinateSpaces.inner_head line 316
  39. theorem OAI.LipschitzCounterexample.CoordinateSpaces.head_eq_sum line 319
  40. theorem OAI.LipschitzCounterexample.CoordinateSpaces.head_tendsto_zero line 341