OAI/Geometry/IsometricImmersion/Caps/CapCutoffGeometry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.Weighted.capOuterSpatialCutoff line 15
2. theorem OAI.SmoothLocal.Weighted.capOuterSpatialCutoff_contDiff line 18
3. theorem OAI.SmoothLocal.Weighted.capOuterSpatialCutoff_range line 22
4. theorem OAI.SmoothLocal.Weighted.capSpatialCutoff_nonzero_bounds line 26
5. theorem OAI.SmoothLocal.Weighted.capOuterSpatialCutoff_one_of_nonzero line 44
6. theorem OAI.SmoothLocal.Weighted.capSpatialCutoff_nonzero_of_partial line 53
7. theorem OAI.SmoothLocal.Weighted.capOuterSpatialCutoff_one_of_partial line 64
8. theorem OAI.SmoothLocal.Flow.modelCurvature_lower_flow_bottom line 75
9. theorem OAI.SmoothLocal.Flow.capChart_not_mem_patchBox_of_cutoff_band line 90
10. theorem OAI.SmoothLocal.Flow.capSpatialCutoff_partial_actual_curvature_lower line 106