OAI/Analysis/RieszRectifiability/Kernel/BoundedBoxBoundary.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Null boundaries of coordinate boxes

The frontier of an open coordinate box lies in the difference between its closed and open versions. Their almost-everywhere equality for volume shows that this frontier has measure zero.

  1. theorem OAI.RieszRectifiability.box_Ioo_frontier_volume_zero line 21
  2. theorem OAI.RieszRectifiability.exhaustionBox_Icc_dist_zero_le line 35
  3. theorem OAI.RieszRectifiability.exhaustionBox_Icc_image_mem_outerBall line 42
  4. theorem OAI.RieszRectifiability.boundedProjectionRegion_preimage_frontier_subset line 52
  5. theorem OAI.RieszRectifiability.boundedProjectionRegion_null_frontier line 74
  6. theorem OAI.RieszRectifiability.boundedProjectionRegion_compact_closure line 82