OAI/Combinatorics/SumProduct/Alignment/CompactFamily01.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CompactFamilyDescent.finite_tests_of_dense_span line 18
  2. theorem OAI.CompactFamilyDescent.continuous_family_descent line 87
  3. theorem OAI.CompactFamilyDescent.continuous_family_map line 96
  4. theorem OAI.CompactFamilyDescent.compact_descended_family line 104
  5. def OAI.CompactFamilyDescent.lipschitzMaps line 114
  6. lemma OAI.CompactFamilyDescent.lipschitz_mul line 116
  7. def OAI.CompactFamilyDescent.lipAlgebra line 136
  8. lemma OAI.CompactFamilyDescent.lipAlgebra_separates line 153
  9. theorem OAI.CompactFamilyDescent.lipschitzMaps_dense line 165
  10. theorem OAI.CompactFamilyDescent.finite_lipschitz_obstruction line 178
  11. abbrev OAI.UniformSquareObservable.ReducedSpace line 198
  12. def OAI.UniformSquareObservable.reducedProjection line 204
  13. def OAI.UniformSquareObservable.observable line 209
  14. lemma OAI.UniformSquareObservable.observable_apply line 224
  15. theorem OAI.UniformSquareObservable.continuous_observable line 235
  16. theorem OAI.UniformSquareObservable.compact_observable_family line 259
  17. theorem OAI.UniformSquareObservable.finite_square_tests line 270