OAI/Geometry/SurfaceImmersion/Atlas/FiniteChartTranslationBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Smallness simultaneously in any fixed finite collection of compact chart regions. The bound is independent of the translated map.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ChartDerivativeClose line 15
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finite_chart_translation_bound line 20