OAI/Combinatorics/BalancedRyser/Local/LocalPrescribedGeometry.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Local.PrescribedGeometry.prescribed_generator_injective line 18
  2. theorem OAI.Balanced.Local.PrescribedGeometry.prescribedPoint_on_left line 24
  3. theorem OAI.Balanced.Local.PrescribedGeometry.prescribedPoint_on_right line 35
  4. theorem OAI.Balanced.Local.PrescribedGeometry.exists_prescribedPoint_on_constituent line 46
  5. theorem OAI.Balanced.Local.PrescribedGeometry.not_onLine_used_constituent line 61
  6. theorem OAI.Balanced.Local.PrescribedGeometry.direction_unused_of_onLine line 74
  7. theorem OAI.Balanced.Local.PrescribedGeometry.mem_prescribedPartners_iff_unused line 82