OAI/Combinatorics/BalancedRyser/Local/AlignedFreeCylinders.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Local.AlignedGlobal.uniform_rectangle_probability line 14
  2. theorem OAI.Balanced.Local.AlignedGlobal.uniform_coordinate_cylinder line 37
  3. def OAI.Balanced.Local.AlignedGlobal.FreePointCylinder line 62
  4. theorem OAI.Balanced.Local.AlignedGlobal.generated_freePointCylinder_iff line 68
  5. theorem OAI.Balanced.Local.AlignedGlobal.aligned_freePointCylinder_unused line 86
  6. theorem OAI.Balanced.Local.AlignedGlobal.aligned_freePointCylinder line 115
  7. theorem OAI.Balanced.Local.AlignedGlobal.original_aligned_freePointCylinder_unused line 125
  8. theorem OAI.Balanced.Local.AlignedGlobal.aligned_unused_conditioned_freePointCylinder line 142