OAI/Geometry/CAT0Fillings/Fillings/WeightedCone.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CAT0Fillings.boundarySucc_neg line 19
  2. lemma OAI.CAT0Fillings.boundarySucc_add line 25
  3. lemma OAI.CAT0Fillings.IsIntegral.neg line 30
  4. lemma OAI.CAT0Fillings.IsIntegral.add line 35
  5. lemma OAI.CAT0Fillings.mass_sub_le line 40
  6. lemma OAI.CAT0Fillings.fillingVolume_zero line 44
  7. lemma OAI.CAT0Fillings.fillingVolume_neg line 50
  8. lemma OAI.CAT0Fillings.fillingVolume_add_le line 60
  9. lemma OAI.CAT0Fillings.fillingVolume_sub_le line 71
  10. lemma OAI.CAT0Fillings.fillingVolume_sub_symm line 79
  11. lemma OAI.CAT0Fillings.fillingVolume_triangle line 86
  12. lemma OAI.CAT0Fillings.abs_fillingVolume_sub_le line 96
  13. lemma OAI.CAT0Fillings.ChartGeometry.density_nonneg line 125
  14. lemma OAI.CAT0Fillings.ChartGeometry.weighted_density_integrable line 128
  15. lemma OAI.CAT0Fillings.ChartGeometry.integral_massMeasure line 136
  16. lemma OAI.CAT0Fillings.ChartGeometry.weighted_density_summable line 150
  17. lemma OAI.CAT0Fillings.ChartGeometry.sweptMass_one_le line 162
  18. theorem OAI.CAT0Fillings.IsCAT0.exists_integral_filling_weighted line 189
  19. lemma OAI.CAT0Fillings.IsMetricCurrent.sub line 212
  20. lemma OAI.CAT0Fillings.currentMassMeasure_sub_le line 217
  21. lemma OAI.CAT0Fillings.integral_dist_massMeasure_sub_le line 225