OAI/Geometry/SurfaceImmersion/Atlas/GridCutoffSupport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The local cell cutoff has the exact global refined support used in phase selection. This keeps the solver's geometry on that original support.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.cellCutoff_eq_vectorPlaneRead line 22
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.cellChartCompact line 44
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.cellChartCompact_subset line 51
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.cellCutoff_tsupport line 55
  5. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.exactCellCutoff line 76
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.exactCellCutoff_apply line 84
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.restore_cell_tsupport line 90