OAI/Analysis/LipschitzHilbert/Phase/AngularBoundaryNull.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Boundary coincidences are a null set of the common translation.

  1. theorem OAI.LipschitzHilbert.AngularGrid.ae_boundaryDistance_pos line 11
  2. theorem OAI.LipschitzHilbert.AngularGrid.ae_normalized_boundaryDistance_pos line 26