OAI/Analysis/LipschitzFree/CompactApproximation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Compact-uniform approximation on bounded separated spaces

  1. theorem OAI.DiscreteFree.evaluation_span_dense line 17
  2. theorem OAI.DiscreteFree.supportProjection_range line 30
  3. theorem OAI.DiscreteFree.supportProjection_finiteRank line 39
  4. theorem OAI.DiscreteFree.span_eventually_fixed line 44
  5. theorem OAI.DiscreteFree.projection_error_bound line 66
  6. theorem OAI.DiscreteFree.projection_pointwise line 77
  7. theorem OAI.DiscreteFree.projection_compact line 93
  8. theorem OAI.DiscreteFree.bounded_separated_hasBAP line 118
  9. theorem OAI.DiscreteFree.hasAP_of_hasBAP line 125