OAI/Analysis/RieszRectifiability/Projections/NonemptyAffineProjection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Affine projection with an explicit nonemptiness witness

This projection takes the plane's nonemptiness as an argument rather than a typeclass assumption. Its displacement is the distance to the plane, and the map is 1-Lipschitz.

  1. def OAI.RieszRectifiability.nonemptyAffineProjection line 19
  2. theorem OAI.RieszRectifiability.nonemptyAffineProjection_dist_self line 24
  3. theorem OAI.RieszRectifiability.nonemptyAffineProjection_lipschitz line 32