OAI/Geometry/SurfaceImmersion/Correction/BundleSmoothingLinearity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Linearity of the concrete finite-atlas bundle smoother.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleLocalize_add line 25
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleLocalize_smul line 31
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleRestore_add line 37
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleRestore_smul line 42
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleSmooth_smul line 48
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleSmooth_add line 58