OAI/CategoryTheory/Thomason/BarycentricMesh.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Barycentric Mesh.

  1. lemma OAI.Thomason.GeometricRecognition.PolyPoint.barycentricLinear_support_eq line 16
  2. lemma OAI.Thomason.GeometricRecognition.PolyPoint.barycentricLinear_eq_zero_iff line 33
  3. lemma OAI.Thomason.GeometricRecognition.PolyPoint.flag_has_max line 48
  4. lemma OAI.Thomason.GeometricRecognition.PolyPoint.flag_union_eq_max line 57
  5. lemma OAI.Thomason.GeometricRecognition.PolyPoint.flag_max_exclusive_vertex line 69
  6. lemma OAI.Thomason.GeometricRecognition.PolyPoint.barycentric_max_minimum line 89
  7. lemma OAI.Thomason.GeometricRecognition.PolyPoint.barycentricLinear_injective_nonneg_flag line 114
  8. lemma OAI.Thomason.GeometricRecognition.PolyPoint.subdivide_injective line 187
  9. instance OAI.Thomason.GeometricRecognition.PolyPoint.finiteChainIndex line 206
  10. lemma OAI.Thomason.GeometricRecognition.PolyPoint.isCompact_chainFace line 214
  11. instance OAI.Thomason.GeometricRecognition.PolyPoint.compactSpace line 230
  12. lemma OAI.Thomason.GeometricRecognition.PolyPoint.embedding_weights line 240
  13. lemma OAI.Thomason.GeometricRecognition.PolyPoint.continuous_iff_weights line 245
  14. instance OAI.Thomason.GeometricRecognition.PolyPoint.finiteBoundedChainIndex line 250
  15. lemma OAI.Thomason.GeometricRecognition.PolyPoint.isCompact_carrier line 264
  16. lemma OAI.Thomason.GeometricRecognition.PolyPoint.isClosed_carrier line 282
  17. lemma OAI.Thomason.GeometricRecognition.PolyPoint.continuous_face_val line 298
  18. lemma OAI.Thomason.GeometricRecognition.PolyPoint.continuous_of_finite_carrier line 314
  19. instance OAI.Thomason.GeometricRecognition.PolyPoint.finiteBoundedFaces line 334
  20. def OAI.Thomason.GeometricRecognition.PolyPoint.allFaces line 343
  21. lemma OAI.Thomason.GeometricRecognition.PolyPoint.mem_allFaces line 347
  22. lemma OAI.Thomason.GeometricRecognition.PolyPoint.subdivide_carrier_iff line 350
  23. lemma OAI.Thomason.GeometricRecognition.PolyPoint.isClosedMap_subdivide line 363
  24. def OAI.Thomason.GeometricRecognition.PolyPoint.subdivisionHomeomorph line 385
  25. def OAI.Thomason.GeometricRecognition.Mesh.average line 400
  26. lemma OAI.Thomason.GeometricRecognition.Mesh.card_smul_average line 402
  27. lemma OAI.Thomason.GeometricRecognition.Mesh.average_sub line 407
  28. lemma OAI.Thomason.GeometricRecognition.Mesh.norm_average_sub_le line 413
  29. lemma OAI.Thomason.GeometricRecognition.Mesh.sum_average_sub line 423
  30. lemma OAI.Thomason.GeometricRecognition.Mesh.average_sub_average line 428
  31. lemma OAI.Thomason.GeometricRecognition.Mesh.norm_average_sub_average_le line 440
  32. def OAI.Thomason.GeometricRecognition.Mesh.ratio line 458
  33. lemma OAI.Thomason.GeometricRecognition.Mesh.ratio_nonneg line 460
  34. lemma OAI.Thomason.GeometricRecognition.Mesh.ratio_lt_one line 464
  35. lemma OAI.Thomason.GeometricRecognition.Mesh.card_ratio_le line 469
  36. lemma OAI.Thomason.GeometricRecognition.Mesh.norm_nested_barycenters_le line 479
  37. def OAI.Thomason.GeometricRecognition.Mesh.ChainBound line 500
  38. lemma OAI.Thomason.GeometricRecognition.Mesh.chainBound_subdivision line 503
  39. def OAI.Thomason.GeometricRecognition.Mesh.Bound line 522
  40. lemma OAI.Thomason.GeometricRecognition.Mesh.bound_subdivision line 525
  41. def OAI.Thomason.GeometricRecognition.Mesh.evaluate line 536
  42. lemma OAI.Thomason.GeometricRecognition.Mesh.evaluate_eq_sum line 539
  43. lemma OAI.Thomason.GeometricRecognition.Mesh.norm_evaluate_sub_le line 543
  44. lemma OAI.Thomason.GeometricRecognition.Mesh.evaluate_barycenter line 562
  45. lemma OAI.Thomason.GeometricRecognition.Mesh.evaluate_subdivide line 568
  46. instance OAI.Thomason.GeometricRecognition.Mesh.finiteChains line 580
  47. def OAI.Thomason.GeometricRecognition.Mesh.level line 584
  48. instance OAI.Thomason.GeometricRecognition.Mesh.finiteLevel line 588
  49. def OAI.Thomason.GeometricRecognition.Mesh.levelHomeomorph line 593
  50. def OAI.Thomason.GeometricRecognition.Mesh.levelVertices line 597
  51. lemma OAI.Thomason.GeometricRecognition.Mesh.chainBound_level line 601
  52. lemma OAI.Thomason.GeometricRecognition.Mesh.bound_level line 607
  53. lemma OAI.Thomason.GeometricRecognition.Mesh.evaluate_levelHomeomorph line 617
  54. lemma OAI.Thomason.GeometricRecognition.Mesh.exists_small_mesh line 627