OAI/Analysis/StrictMeans/BoundaryCells.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.scaled_integer_cells_disjoint line 94
  2. lemma OAI.StrictInverseFirstPower.volume_scaled_integer_cell line 110
  3. lemma OAI.StrictInverseFirstPower.cell_disks_measure_bound line 116
  4. def OAI.StrictInverseFirstPower.cellRectangle line 150
  5. lemma OAI.StrictInverseFirstPower.isCompact_cellRectangle line 153
  6. lemma OAI.StrictInverseFirstPower.family_rectangle_bound line 175
  7. lemma OAI.StrictInverseFirstPower.full_ball_halfplane_subset line 185
  8. lemma OAI.StrictInverseFirstPower.omitted_derivative_bound line 193
  9. lemma OAI.StrictInverseFirstPower.cell_rebased_mem line 214
  10. lemma OAI.StrictInverseFirstPower.omitted_cell_comparison line 235
  11. lemma OAI.StrictInverseFirstPower.omitted_cell_power_bound line 255
  12. def OAI.StrictInverseFirstPower.boundaryWitness line 279
  13. def OAI.StrictInverseFirstPower.boundaryBadScale line 283
  14. def OAI.StrictInverseFirstPower.boundaryMarkedCells line 286
  15. def OAI.StrictInverseFirstPower.cellMidpointImage line 289
  16. lemma OAI.StrictInverseFirstPower.same_cell_difference line 292
  17. lemma OAI.StrictInverseFirstPower.midpoint_mem_cell line 298
  18. lemma OAI.StrictInverseFirstPower.floor_cell_mem line 302
  19. lemma OAI.StrictInverseFirstPower.boundaryBadScale_subset_cover line 308
  20. lemma OAI.StrictInverseFirstPower.marked_segments_image_bounded line 322
  21. lemma OAI.StrictInverseFirstPower.cell_area_power_identity line 340
  22. theorem OAI.StrictInverseFirstPower.boundaryBadScale_measure_bound line 346