OAI/Combinatorics/HadwigerCounterexample/RealizationConditions.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Realization Conditions

  1. def OAI.HadwigerCounterexample.Volley.legal line 16
  2. def OAI.HadwigerCounterexample.Volley.diagonalAt line 17
  3. def OAI.HadwigerCounterexample.Volley.bounded line 18
  4. structure OAI.HadwigerCounterexample.Volley.scalarRecipe line 22

    Source documentation

    Conditions for one orientation of roles, §5 (scalar recipe).

    structure scalarRecipe (t : Tagging p I) (m : Mixer p n) (x : UnitType p n N) (S : Plan p n)
    (M : Cross p n) : Prop where
…

    Mentions: OAI.HadwigerCounterexample.Tagging, OAI.HadwigerCounterexample.Mixer, OAI.HadwigerCounterexample.UnitType, OAI.HadwigerCounterexample.Plan, OAI.HadwigerCounterexample.Cross

  5. def OAI.HadwigerCounterexample.Volley.roleMatch line 30
  6. def OAI.HadwigerCounterexample.Volley.attackGrad line 33
  7. def OAI.HadwigerCounterexample.Volley.realized line 38
  8. theorem OAI.HadwigerCounterexample.Volley.shoots_swap line 41
  9. theorem OAI.HadwigerCounterexample.Volley.sum_share line 44
  10. theorem OAI.HadwigerCounterexample.Volley.sum_mem line 55
  11. theorem OAI.HadwigerCounterexample.Volley.realized_conflicts line 59
  12. def OAI.HadwigerCounterexample.scalarBlocks line 74
  13. theorem OAI.HadwigerCounterexample.contract_val line 77
  14. theorem OAI.HadwigerCounterexample.contract_scalars line 85