OAI/Geometry/CylinderCovering/Rational/Domain.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SlopeRational.ceilingPolynomial_continuous line 11
  2. lemma OAI.SlopeRational.labelDomain_bounds line 15
  3. lemma OAI.SlopeRational.wedge_isClosed line 21
  4. lemma OAI.SlopeRational.labelDomain_isClosed line 25
  5. lemma OAI.SlopeRational.labelDomain_isCompact line 34
  6. lemma OAI.SlopeRational.labelDomain_measurableSet line 45
  7. lemma OAI.SlopeRational.labelDomain_mem_iff line 48
  8. lemma OAI.SlopeRational.labelDomain_vertical_section line 59
  9. lemma OAI.SlopeRational.labelDomain_volume_ne_top line 66
  10. def OAI.SlopeRational.DomainGeometry.pairEquiv line 72
  11. lemma OAI.SlopeRational.DomainGeometry.pairEquiv_measurePreserving line 75
  12. lemma OAI.SlopeRational.DomainGeometry.volume_graph_eq_zero line 78
  13. lemma OAI.SlopeRational.frontier_labelDomain_subset line 94
  14. lemma OAI.SlopeRational.volume_frontier_labelDomain line 125
  15. lemma OAI.SlopeRational.labelDomain_volume_le line 136
  16. lemma OAI.SlopeRational.labelDomain_realVolume_le line 155