OAI/Geometry/SurfaceImmersion/Atlas/WeightedProjectionLinearization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Positive scalar weights do not alter the crosscap linearization at a projection kernel, except by the same nonzero scalar factor.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.weightedJet_product_germ line 14
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.directionJetLinearization_congr_germ line 23
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.projected_directionJet_scaled line 30
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.regular_weighted_directionJet line 48