OAI/Geometry/SmoothYau/Smoothness/ChartTensorCoordLocal1.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.YauCounterexamples.ContinuousSmoothFamilyOn line 18
  2. lemma OAI.YauCounterexamples.ContinuousSmoothFamilyOn.value line 24
  3. lemma OAI.YauCounterexamples.ContinuousSmoothFamilyOn.postcomp line 30
  4. lemma OAI.YauCounterexamples.ContinuousSmoothFamilyOn.prodMk line 53
  5. lemma OAI.YauCounterexamples.ContinuousSmoothFamilyOn.fderiv line 63
  6. lemma OAI.YauCounterexamples.ContinuousSmoothFamilyOn.const line 73
  7. lemma OAI.YauCounterexamples.ContinuousSmoothFamilyOn.scalar_const line 79
  8. lemma OAI.YauCounterexamples.ContinuousSmoothFamilyOn.add line 88
  9. lemma OAI.YauCounterexamples.ContinuousSmoothFamilyOn.mul line 92
  10. lemma OAI.YauCounterexamples.ContinuousSmoothFamilyOn.inv line 96
  11. lemma OAI.YauCounterexamples.ContinuousSmoothFamilyOn.sqrt line 100
  12. lemma OAI.YauCounterexamples.compactSmooth_uniformity_countable line 116
  13. lemma OAI.YauCounterexamples.compactSmooth_t2 line 120
  14. def OAI.YauCounterexamples.compactSmoothMetricSpace line 127
  15. lemma OAI.YauCounterexamples.compactSmooth_continuousJets line 131
  16. lemma OAI.YauCounterexamples.compactSmooth_family line 138
  17. lemma OAI.YauCounterexamples.ContinuousSmoothFamilyOn.sum line 152
  18. lemma OAI.YauCounterexamples.ContinuousSmoothFamilyOn.prod line 161
  19. lemma OAI.YauCounterexamples.ContinuousSmoothFamilyOn.neg line 170
  20. lemma OAI.YauCounterexamples.ContinuousSmoothFamilyOn.sub line 173
  21. lemma OAI.YauCounterexamples.ContinuousSmoothFamilyOn.mono line 176
  22. lemma OAI.YauCounterexamples.ContinuousSmoothFamilyOn.of_local line 179
  23. lemma OAI.YauCounterexamples.ContinuousSmoothFamilyOn.congr line 190
  24. lemma OAI.YauCounterexamples.family_metricDet line 207
  25. lemma OAI.YauCounterexamples.family_metricDensity line 217
  26. lemma OAI.YauCounterexamples.family_metricInverse line 220
  27. lemma OAI.YauCounterexamples.family_metricFirstCoefficient line 237
  28. theorem OAI.YauCounterexamples.continuous_schwartz_common_support line 250
  29. def OAI.YauCounterexamples.chartTrivMetricForm line 307
  30. lemma OAI.YauCounterexamples.contDiffAt_chartTrivMetricForm line 311
  31. lemma OAI.YauCounterexamples.chartTrivMetricForm_pairing line 324
  32. lemma OAI.YauCounterexamples.chartTrivMetricForm_pos line 332
  33. def OAI.YauCounterexamples.chartTensorPositive line 345
  34. lemma OAI.YauCounterexamples.chartTensorPositive_zero line 350
  35. lemma OAI.YauCounterexamples.isOpen_chartTensorPositive line 357
  36. lemma OAI.YauCounterexamples.chartTensorForm_pos line 374
  37. def OAI.YauCounterexamples.chartTensorMetric line 405
  38. def OAI.YauCounterexamples.chartTensorOfMetric line 442
  39. lemma OAI.YauCounterexamples.chartTensorOfMetric_isSymm line 461
  40. lemma OAI.YauCounterexamples.chartTensorOfMetric_positive line 471
  41. lemma OAI.YauCounterexamples.smoothMetric_ext line 482
  42. lemma OAI.YauCounterexamples.chartTensorMetric_ofMetric line 491
  43. lemma OAI.YauCounterexamples.chartMetricForm_chartTensorMetric line 538
  44. lemma OAI.YauCounterexamples.metricCoefficient_chartTensorMetric line 552
  45. lemma OAI.YauCounterexamples.family_chartTensorMetric_main line 564
  46. lemma OAI.YauCounterexamples.continuousSmoothFamily_from_chart line 599
  47. lemma OAI.YauCounterexamples.family_chartTensorMetric line 684