OAI/Combinatorics/ThinTrees/FixedPoint.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.StrongThinTree.FixedPoint.Chain line 13
  2. def OAI.StrongThinTree.FixedPoint.face line 17
  3. def OAI.StrongThinTree.FixedPoint.boundary line 19
  4. lemma OAI.StrongThinTree.FixedPoint.boundary_face line 22
  5. lemma OAI.StrongThinTree.FixedPoint.boundary_empty line 25
  6. def OAI.StrongThinTree.FixedPoint.cone line 28
  7. lemma OAI.StrongThinTree.FixedPoint.cone_face line 32
  8. lemma OAI.StrongThinTree.FixedPoint.add_self line 37
  9. lemma OAI.StrongThinTree.FixedPoint.boundary_cone_face line 41
  10. lemma OAI.StrongThinTree.FixedPoint.boundary_cone line 61
  11. lemma OAI.StrongThinTree.FixedPoint.boundary_cone_eq line 71
  12. lemma OAI.StrongThinTree.FixedPoint.boundary_boundary_face line 76
  13. lemma OAI.StrongThinTree.FixedPoint.boundary_boundary line 84
  14. def OAI.StrongThinTree.FixedPoint.subdivFace line 92
  15. def OAI.StrongThinTree.FixedPoint.subdivision line 98
  16. lemma OAI.StrongThinTree.FixedPoint.subdivision_face line 101
  17. lemma OAI.StrongThinTree.FixedPoint.subdiv_empty line 104
  18. lemma OAI.StrongThinTree.FixedPoint.subdiv_nonempty line 106
  19. lemma OAI.StrongThinTree.FixedPoint.boundary_subdivFace line 112
  20. lemma OAI.StrongThinTree.FixedPoint.boundary_subdivision line 131
  21. def OAI.StrongThinTree.FixedPoint.rename line 143
  22. lemma OAI.StrongThinTree.FixedPoint.rename_face line 149
  23. lemma OAI.StrongThinTree.FixedPoint.rename_cone_face line 154
  24. lemma OAI.StrongThinTree.FixedPoint.rename_cone line 173
  25. lemma OAI.StrongThinTree.FixedPoint.boundary_rename_face line 182
  26. lemma OAI.StrongThinTree.FixedPoint.boundary_rename line 191
  27. def OAI.StrongThinTree.FixedPoint.Supported line 200
  28. lemma OAI.StrongThinTree.FixedPoint.supported_zero line 204
  29. lemma OAI.StrongThinTree.FixedPoint.supported_face line 208
  30. lemma OAI.StrongThinTree.FixedPoint.supported_add line 215
  31. lemma OAI.StrongThinTree.FixedPoint.supported_smul line 221
  32. lemma OAI.StrongThinTree.FixedPoint.supported_sum line 227
  33. lemma OAI.StrongThinTree.FixedPoint.chain_expansion line 239
  34. lemma OAI.StrongThinTree.FixedPoint.supported_map line 244
  35. lemma OAI.StrongThinTree.FixedPoint.supported_cone line 258
  36. lemma OAI.StrongThinTree.FixedPoint.supported_mono line 269
  37. def OAI.StrongThinTree.FixedPoint.Flag line 274
  38. lemma OAI.StrongThinTree.FixedPoint.subdiv_supported line 278
  39. lemma OAI.StrongThinTree.FixedPoint.supported_rename line 315
  40. lemma OAI.StrongThinTree.FixedPoint.boundary_face_erase line 327
  41. lemma OAI.StrongThinTree.FixedPoint.supported_singleton_eq line 337
  42. theorem OAI.StrongThinTree.FixedPoint.sperner_chain line 344
  43. lemma OAI.StrongThinTree.FixedPoint.map_coefficient_witness line 381
  44. theorem OAI.StrongThinTree.FixedPoint.sperner_witness line 393
  45. def OAI.StrongThinTree.FixedPoint.IterV line 410
  46. instance OAI.StrongThinTree.FixedPoint.iterVDecidableEq line 414
  47. def OAI.StrongThinTree.FixedPoint.iterSubdivision line 420
  48. lemma OAI.StrongThinTree.FixedPoint.boundary_iterSubdivision line 424
  49. lemma OAI.StrongThinTree.FixedPoint.iterSubdivision_empty line 433
  50. def OAI.StrongThinTree.FixedPoint.mean line 441
  51. lemma OAI.StrongThinTree.FixedPoint.mean_nonneg line 444
  52. lemma OAI.StrongThinTree.FixedPoint.mean_zero line 448
  53. lemma OAI.StrongThinTree.FixedPoint.mean_difference line 452
  54. lemma OAI.StrongThinTree.FixedPoint.mean_mesh line 467
  55. def OAI.StrongThinTree.FixedPoint.CoordFace line 520
  56. def OAI.StrongThinTree.FixedPoint.baryPoint line 523
  57. lemma OAI.StrongThinTree.FixedPoint.coordFace_bary line 528
  58. def OAI.StrongThinTree.FixedPoint.iterPoint line 545
  59. def OAI.StrongThinTree.FixedPoint.meshFactor line 549
  60. lemma OAI.StrongThinTree.FixedPoint.meshFactor_nonneg line 551
  61. lemma OAI.StrongThinTree.FixedPoint.meshFactor_lt_one line 558
  62. def OAI.StrongThinTree.FixedPoint.GeometricFacet line 564
  63. lemma OAI.StrongThinTree.FixedPoint.iterSubdivision_supported line 569
  64. def OAI.StrongThinTree.FixedPoint.simplex line 620
  65. lemma OAI.StrongThinTree.FixedPoint.simplex_label line 625
  66. abbrev OAI.StrongThinTree.FixedPoint.Delta line 647
  67. theorem OAI.StrongThinTree.FixedPoint.simplex_approximation line 649
  68. theorem OAI.StrongThinTree.FixedPoint.simplex_fixed_point line 697
  69. theorem OAI.StrongThinTree.FixedPoint.compact_convex_approximation line 749
  70. theorem OAI.StrongThinTree.FixedPoint.compact_convex_fixed_point line 818