OAI/Geometry/LatticeCovering/Covering.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SingleLatticeCovering.CoverGeometry.quotient_hole_bound line 16
  2. lemma OAI.SingleLatticeCovering.CoverGeometry.quotient_real_hole_bound line 57
  3. theorem OAI.SingleLatticeCovering.CoverGeometry.joined_holes_to_cover line 73
  4. theorem OAI.SingleLatticeCovering.CoverGeometry.finite_patterns_to_cover line 104
  5. lemma OAI.SingleLatticeCovering.Vertical.Block.integer_mem line 141
  6. lemma OAI.SingleLatticeCovering.Vertical.Chain.raw_integer_mem line 155
  7. lemma OAI.SingleLatticeCovering.Vertical.Chain.full_raw_integer_mem line 163
  8. def OAI.SingleLatticeCovering.Vertical.Chain.alphabetSeq line 168
  9. lemma OAI.SingleLatticeCovering.Vertical.Chain.alphabetSeq_fin line 171
  10. theorem OAI.SingleLatticeCovering.Vertical.prepared_chain_to_cover line 185
  11. lemma OAI.SingleLatticeCovering.Vertical.Chain.det_pos line 250
  12. theorem OAI.SingleLatticeCovering.Vertical.labeled_chain_to_cover line 257
  13. lemma OAI.SingleLatticeCovering.LatticeGeometry.affine_image_volume line 325
  14. lemma OAI.SingleLatticeCovering.LatticeGeometry.affine_image_cover line 333
  15. lemma OAI.SingleLatticeCovering.LatticeGeometry.affine_image_density line 350
  16. lemma OAI.SingleLatticeCovering.LatticeGeometry.affineEquiv_eq_linear_add line 367
  17. lemma OAI.SingleLatticeCovering.LatticeGeometry.pull_back_cover line 374
  18. lemma OAI.SingleLatticeCovering.Sections.compact_separated_cover line 406
  19. lemma OAI.SingleLatticeCovering.Sections.separated_card_bound line 425
  20. lemma OAI.SingleLatticeCovering.Sections.ball_finite_net line 473
  21. def OAI.SingleLatticeCovering.Sections.fiber line 523
  22. lemma OAI.SingleLatticeCovering.Sections.fiber_compact line 525
  23. lemma OAI.SingleLatticeCovering.Sections.fiber_convex line 537
  24. lemma OAI.SingleLatticeCovering.Sections.nearby_fiber_inclusion line 546
  25. lemma OAI.SingleLatticeCovering.Sections.shrink_power_half line 575
  26. lemma OAI.SingleLatticeCovering.Sections.prescribed_volume line 590