OAI/Combinatorics/VariableWL/BlockGame.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.VariableWL.Blocks.RingSystem line 12
  2. abbrev OAI.VariableWL.Blocks.TypeAddress line 19
  3. def OAI.VariableWL.Blocks.siteRing line 22
  4. def OAI.VariableWL.Blocks.leftAddress line 25
  5. def OAI.VariableWL.Blocks.rightAddress line 29
  6. def OAI.VariableWL.Blocks.squareRing line 33
  7. def OAI.VariableWL.Blocks.ringSum line 37
  8. def OAI.VariableWL.Blocks.Attained line 40
  9. theorem OAI.VariableWL.Blocks.attained_nonempty line 43
  10. theorem OAI.VariableWL.Blocks.agree_carries line 46
  11. theorem OAI.VariableWL.Blocks.copy_left line 54
  12. theorem OAI.VariableWL.Blocks.copy_right line 62
  13. theorem OAI.VariableWL.Blocks.squareRing_vertical line 70
  14. theorem OAI.VariableWL.Blocks.squareRing_equation line 79
  15. theorem OAI.VariableWL.Blocks.agree_symm line 100
  16. theorem OAI.VariableWL.Blocks.attained_link_forward line 104
  17. theorem OAI.VariableWL.Blocks.attained_link_reverse line 117
  18. theorem OAI.VariableWL.Blocks.affine_of_boundary line 136
  19. theorem OAI.VariableWL.Blocks.attained_link_images line 140
  20. def OAI.VariableWL.Blocks.realAddress line 153
  21. def OAI.VariableWL.Blocks.internalAddress line 156
  22. def OAI.VariableWL.Blocks.realAttained line 159
  23. def OAI.VariableWL.Blocks.scalarAttained line 162
  24. def OAI.VariableWL.Blocks.addressedAttained line 166
  25. theorem OAI.VariableWL.Blocks.addressedAttained_eq line 170
  26. theorem OAI.VariableWL.Blocks.dependent_linear_image line 175
  27. theorem OAI.VariableWL.Blocks.left_image_evaluation line 182
  28. theorem OAI.VariableWL.Blocks.right_image_evaluation line 200
  29. theorem OAI.VariableWL.Blocks.wire_images line 218
  30. theorem OAI.VariableWL.Blocks.attained_first line 231
  31. theorem OAI.VariableWL.Blocks.attained_last line 241
  32. theorem OAI.VariableWL.Blocks.attained_internal line 252
  33. def OAI.VariableWL.Blocks.extractedWitness line 264
  34. def OAI.VariableWL.General.attainedRings line 285
  35. theorem OAI.VariableWL.General.consistent_of_winning line 306
  36. theorem OAI.VariableWL.General.positive_order line 311
  37. theorem OAI.VariableWL.General.equivalent_iff_consistent line 318