OAI/Geometry/CAT0Fillings/Fillings/Attainment.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CAT0Fillings.Slicing.NormalApprox.boundarySucc line 18
  2. lemma OAI.CAT0Fillings.Slicing.NormalApprox.integerRectifiable line 32
  3. theorem OAI.CAT0Fillings.Slicing.NormalApprox.integral line 38
  4. theorem OAI.CAT0Fillings.Slicing.integral_weak_closed line 45
  5. theorem OAI.CAT0Fillings.Slicing.exists_integral_weak_subsequence line 66
  6. theorem OAI.CAT0Fillings.mass_le_of_mass_tendsto line 91
  7. def OAI.CAT0Fillings.fillingVolume line 105
  8. lemma OAI.CAT0Fillings.fillingVolume_nonneg line 109
  9. lemma OAI.CAT0Fillings.fillingVolume_le line 116
  10. theorem OAI.CAT0Fillings.exists_filling_mass_eq line 124
  11. theorem OAI.CAT0Fillings.IsCAT0.exists_minimal_integral_filling line 148
  12. lemma OAI.CAT0Fillings.IsCAT0.fillingVolume_le_linear line 155