OAI/Geometry/IsometricImmersion/Pulses/ShearedPulseRegions.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Pulse.shearedModelSquare line 15
  2. theorem OAI.SmoothLocal.Pulse.shearedModelSquare_eq_image line 18
  3. theorem OAI.SmoothLocal.Pulse.shearedModelSquare_isCompact line 27
  4. theorem OAI.SmoothLocal.Pulse.shearedModelSquare_subset_domain line 31
  5. theorem OAI.SmoothLocal.Pulse.sheared_reference_metric_smoothPositive line 34
  6. theorem OAI.SmoothLocal.Pulse.shearedModelDomain_isOpen line 41
  7. def OAI.SmoothLocal.Pulse.sectionFourClosedSlab line 45
  8. theorem OAI.SmoothLocal.Pulse.sectionFourClosedSlab_mem_shearedModelSquare line 48
  9. theorem OAI.SmoothLocal.Pulse.pulseRectangle_mem_shearedModelSquare line 67
  10. theorem OAI.SmoothLocal.Pulse.pulseRectangle_eventually_in_shearedModelSquare line 78
  11. theorem OAI.SmoothLocal.Pulse.shrinkingSlab_subset_sectionFourClosedSlab line 97