OAI/Geometry/SmoothYau/SphereMetric/ThreeFixedFormNorm.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.threeManifold_preconnected line 19
  2. lemma OAI.YauCounterexamples.three_rank_separating_tensor line 24
  3. theorem OAI.YauCounterexamples.three_nondegenerate_pinning_tensor line 94
  4. theorem OAI.YauCounterexamples.exists_three_simple_pinned_family line 142
  5. def OAI.YauCounterexamples.threeTensorSupport line 221
  6. abbrev OAI.YauCounterexamples.ThreeTensor line 223
  7. def OAI.YauCounterexamples.ThreeExterior line 224
  8. lemma OAI.YauCounterexamples.threeTensorSupport_image line 226
  9. lemma OAI.YauCounterexamples.ThreeExterior.mono line 232
  10. lemma OAI.YauCounterexamples.threeExterior_support line 236
  11. def OAI.YauCounterexamples.threeTensorOf line 242
  12. lemma OAI.YauCounterexamples.threeTensorOf_zero line 246
  13. def OAI.YauCounterexamples.threePositiveSet line 251
  14. abbrev OAI.YauCounterexamples.ThreePositiveTensor line 253
  15. def OAI.YauCounterexamples.threeTensorMetric line 254
  16. lemma OAI.YauCounterexamples.threePositiveSet_isOpen line 257
  17. lemma OAI.YauCounterexamples.threeTensorOf_positive line 260
  18. lemma OAI.YauCounterexamples.threeTensorMetric_of line 264
  19. lemma OAI.YauCounterexamples.threePositive_zero line 269
  20. lemma OAI.YauCounterexamples.threeTensorMetric_zero line 271
  21. lemma OAI.YauCounterexamples.threeTensorMetric_family line 273
  22. lemma OAI.YauCounterexamples.exists_three_open_model line 279
  23. def OAI.YauCounterexamples.ThreeRegular line 302
  24. def OAI.YauCounterexamples.ThreeSimple line 304
  25. def OAI.YauCounterexamples.threeCollar line 307
  26. lemma OAI.YauCounterexamples.threeCollar_isOpen line 309
  27. lemma OAI.YauCounterexamples.threeCollar_nonempty line 311
  28. lemma OAI.YauCounterexamples.three_exterior_profile_pair line 316
  29. lemma OAI.YauCounterexamples.three_clean_collar_gradient line 329
  30. lemma OAI.YauCounterexamples.three_collar_rank line 343
  31. theorem OAI.YauCounterexamples.three_pin_near line 368
  32. def OAI.YauCounterexamples.ThreeSignAbove line 411
  33. def OAI.YauCounterexamples.ThreeLargeWitness line 417
  34. lemma OAI.YauCounterexamples.three_largeWitness_eventually line 421
  35. lemma OAI.YauCounterexamples.three_regular_nonzero line 449
  36. theorem OAI.YauCounterexamples.exists_three_simple_stage line 456
  37. theorem OAI.YauCounterexamples.exists_three_fixed_witnesses line 524