OAI/Geometry/IntegralFillings/Currents/Basic.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpIntegralFillings.BoundedLip.continuous line 22
  2. lemma OAI.SharpIntegralFillings.BoundedLip.const line 26
  3. lemma OAI.SharpIntegralFillings.BoundedLip.add line 30
  4. lemma OAI.SharpIntegralFillings.BoundedLip.const_mul line 39
  5. lemma OAI.SharpIntegralFillings.isMetricCurrent_zero line 55
  6. lemma OAI.SharpIntegralFillings.mass_nonneg line 66
  7. lemma OAI.SharpIntegralFillings.mass_le_measure line 71
  8. lemma OAI.SharpIntegralFillings.mass_zero line 79
  9. lemma OAI.SharpIntegralFillings.boundarySucc_zero line 88
  10. lemma OAI.SharpIntegralFillings.boundary_zero line 94
  11. def OAI.SharpIntegralFillings.emptyChart line 100
  12. lemma OAI.SharpIntegralFillings.emptyChart_image line 116
  13. lemma OAI.SharpIntegralFillings.emptyChart_action line 121
  14. lemma OAI.SharpIntegralFillings.integerRectifiable_zero line 126
  15. lemma OAI.SharpIntegralFillings.isIntegral_zero line 139
  16. lemma OAI.SharpIntegralFillings.compactlySupported_zero line 151
  17. lemma OAI.SharpIntegralFillings.isCycle_zero line 156