OAI/Geometry/SurfaceImmersion/Correction/FiniteSmootherLinearity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Linearity of the actual finite-order smoothing construction.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.residual_add line 14
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.residual_smul line 25
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteSmooth_add line 32
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteSmooth_smul line 38