OAI/Geometry/CAT0Fillings/Prism/ClosedCylinder.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CAT0Fillings.ClosedCylinder line 36
  2. def OAI.CAT0Fillings.cylinderClamp line 37
  3. def OAI.CAT0Fillings.cylinderEmbed line 39
  4. lemma OAI.CAT0Fillings.cylinderClamp_lipschitz line 41
  5. lemma OAI.CAT0Fillings.cylinderEmbed_isometry line 51
  6. lemma OAI.CAT0Fillings.cylinderEmbed_clamp line 55
  7. lemma OAI.CAT0Fillings.IntegerChart.prism_clamp_bilipschitz line 63
  8. def OAI.CAT0Fillings.IntegerChart.closedPrism line 77
  9. lemma OAI.CAT0Fillings.IntegerChart.closedPrism_action line 80
  10. lemma OAI.CAT0Fillings.IntegerChart.closedPrism_image line 83
  11. lemma OAI.CAT0Fillings.IntegerChart.closedPrism_image_disjoint line 86
  12. lemma OAI.CAT0Fillings.IntegerChart.mass_closedPrism_le line 98