OAI/Analysis/RieszRectifiability/Projections/ProjectionDiskLift.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Projection between subspace disks

Projecting a displacement orthogonally and translating its center carries a closed disk into a disk of the same radius. The disk lift records this range constraint.

  1. def OAI.RieszRectifiability.projectionDiskLift line 19
  2. theorem OAI.RieszRectifiability.projectionDiskLift_sub line 30
  3. theorem OAI.RieszRectifiability.projectionDiskLift_lipschitz line 44
  4. theorem OAI.RieszRectifiability.projectionDiskLift_center line 53