OAI/Combinatorics/HadwigerCounterexample/AttackCutDecomposition.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Attack Cut Decomposition

  1. theorem OAI.HadwigerCounterexample.colSp_kill line 14
  2. theorem OAI.HadwigerCounterexample.box_kill line 25
  3. theorem OAI.HadwigerCounterexample.orth_sub line 29
  4. theorem OAI.HadwigerCounterexample.orth_sum line 33
  5. def OAI.HadwigerCounterexample.Volley.strike line 43
  6. theorem OAI.HadwigerCounterexample.Volley.strike_here line 46
  7. theorem OAI.HadwigerCounterexample.Volley.strike_pair line 60
  8. theorem OAI.HadwigerCounterexample.Volley.strike_orth line 74
  9. def OAI.HadwigerCounterexample.labStruct line 96
  10. theorem OAI.HadwigerCounterexample.struct_tri line 101
  11. theorem OAI.HadwigerCounterexample.Volley.orth_structure line 137
  12. theorem OAI.HadwigerCounterexample.Volley.edge_at line 160
  13. theorem OAI.HadwigerCounterexample.Volley.cut_tri line 168
  14. theorem OAI.HadwigerCounterexample.Volley.structure_mark line 179
  15. def OAI.HadwigerCounterexample.Volley.clean line 233

    Source documentation

    a component uses at most R nonattack labels.

    def clean (v : Volley p n I) (i : Bool) (R : ℕ) (M : Moment p n) :=
…

    Mentions: OAI.HadwigerCounterexample.Volley, OAI.HadwigerCounterexample.Moment

  16. theorem OAI.HadwigerCounterexample.Volley.split_orth line 237