OAI/Geometry/CylinderCovering/Ruled/CellGeometry.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ProductCells.closedCell_isClosed line 10
  2. lemma OAI.ProductCells.openCell_isOpen line 15
  3. lemma OAI.ProductCells.closedCell_subset_box line 20
  4. lemma OAI.ProductCells.closedCell_isCompact line 26
  5. lemma OAI.ProductCells.openCell_subset_closedCell line 29
  6. lemma OAI.ProductCells.openCell_isBounded line 33
  7. lemma OAI.ProductCells.dilation_closedCell line 36
  8. lemma OAI.ProductCells.dilation_openCell line 61
  9. lemma OAI.ProductCells.logarithmicCell_eq_dilation line 86
  10. lemma OAI.ProductCells.logarithmicIntercept_eq_dilation line 91
  11. lemma OAI.ProductCells.opposite_expansion_bounds line 98
  12. lemma OAI.ProductCells.perturbed_product_bounds line 116
  13. lemma OAI.ProductCells.expanded_parameterCell_mem_intercept line 147
  14. lemma OAI.ProductCells.quadrant_integral line 155
  15. lemma OAI.ProductCells.areaRatio_exp line 167
  16. lemma OAI.ProductCells.areaRatio_exp_tendsto line 186
  17. lemma OAI.ProductCells.areaRatio_tendsto_zero line 200
  18. lemma OAI.ProductCells.exists_parameter_after_padding line 210
  19. lemma OAI.ProductCells.areaRatio_continuousAt_padding_zero line 224
  20. lemma OAI.ProductCells.exists_padding_after_parameter line 240
  21. lemma OAI.ProductCells.exists_logarithmic_parameters line 257