OAI/Geometry/CAT0Fillings/Slices/WeakApproximation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CAT0Fillings.Slicing.NormalApprox line 17
  2. lemma OAI.CAT0Fillings.Slicing.normalApprox_of_weak_limit line 23
  3. def OAI.CAT0Fillings.Slicing.denseCurrentTest line 33
  4. lemma OAI.CAT0Fillings.Slicing.denseCurrentTest_dense line 36
  5. def OAI.CAT0Fillings.Slicing.currentCoordinates line 40
  6. def OAI.CAT0Fillings.Slicing.normalApproxClosed line 43
  7. lemma OAI.CAT0Fillings.Slicing.lipschitz_of_dense_limit line 47
  8. lemma OAI.CAT0Fillings.Slicing.IsMetricCurrent.testClass_lipschitz_zero line 60
  9. lemma OAI.CAT0Fillings.Slicing.IsIntegral.uniform_testClass_lipschitz line 79
  10. lemma OAI.CAT0Fillings.Slicing.weak_limit_of_coordinate_limit line 89
  11. theorem OAI.CAT0Fillings.Slicing.normalApprox_iff_coordinates line 119
  12. lemma OAI.CAT0Fillings.Slicing.measurableSet_normalApprox line 140
  13. lemma OAI.CAT0Fillings.Slicing.continuous_profile_action line 171
  14. lemma OAI.CAT0Fillings.Slicing.measurable_profile_action_family line 197
  15. lemma OAI.CAT0Fillings.Slicing.measurable_restriction_family line 207
  16. theorem OAI.CAT0Fillings.Slicing.measurable_superlevelSlice_family line 231