OAI/Geometry/TamingCompatibility/Charts/ChartUnitaryData.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.TamingCompatibility.GeometricChart.Data line 20
  2. theorem OAI.TamingCompatibility.GeometricChart.data_nonempty line 49
  3. def OAI.TamingCompatibility.GeometricChart.data line 62
  4. def OAI.TamingCompatibility.GeometricChart.Data.source line 68
  5. lemma OAI.TamingCompatibility.GeometricChart.Data.source_open line 70
  6. lemma OAI.TamingCompatibility.GeometricChart.Data.mem_source line 72
  7. lemma OAI.TamingCompatibility.GeometricChart.Data.source_subset line 73
  8. lemma OAI.TamingCompatibility.GeometricChart.Data.source_image_subset line 74
  9. lemma OAI.TamingCompatibility.GeometricChart.Data.small_ball_subset line 78
  10. theorem OAI.TamingCompatibility.GeometricChart.finite_data_partition line 82
  11. lemma OAI.TamingCompatibility.GeometricChart.coordinateSupport_small line 120
  12. lemma OAI.TamingCompatibility.GeometricChart.coordinateSupport_domain line 126
  13. lemma OAI.TamingCompatibility.GeometricChart.localizedFunction_zero_off line 130
  14. def OAI.TamingCompatibility.GeometricChart.scalar line 141
  15. lemma OAI.TamingCompatibility.GeometricChart.scalar_zero_off line 145
  16. lemma OAI.TamingCompatibility.GeometricChart.scalar_tsupport_subset line 154
  17. lemma OAI.TamingCompatibility.GeometricChart.scalar_smooth_compact line 163
  18. def OAI.TamingCompatibility.GeometricChart.scalarSchwartz line 174
  19. lemma OAI.TamingCompatibility.GeometricChart.scalarSchwartz_support line 180