OAI/Geometry/Cannon/Modulus/BoundaryNormalizedAnnularCarriers.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CannonRelease.boundary_normalized_annular_carriers line 17
  2. lemma OAI.CannonTileTopology.regular_tiles_inter_frontier line 58
  3. lemma OAI.CannonTileTopology.disk_center_tile_incidence line 67
  4. lemma OAI.CannonTileTopology.compact_trace line 83
  5. lemma OAI.CannonTileTopology.image_regular line 92
  6. lemma OAI.CannonTileTopology.trace_frontier line 97
  7. lemma OAI.CannonTileTopology.trace_regular line 103
  8. lemma OAI.CannonTileTopology.coe_image_interior line 116
  9. lemma OAI.CannonTileTopology.coe_closure_interior line 127
  10. lemma OAI.CannonTileTopology.coe_regular line 134
  11. lemma OAI.CannonTileTopology.coe_frontier line 138
  12. lemma OAI.CannonTileTopology.coe_interior_frontier line 143
  13. lemma OAI.CannonTileTopology.segment_two_closedBalls line 150