OAI/Combinatorics/VariableWL/ProductImages.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.VariableWL.ProductImages.Instance line 13
  2. abbrev OAI.VariableWL.ProductImages.Instance.Address line 30
  3. def OAI.VariableWL.ProductImages.Instance.Allowed line 32
  4. def OAI.VariableWL.ProductImages.Instance.mapAddress line 34
  5. def OAI.VariableWL.ProductImages.Instance.leftForm line 36
  6. def OAI.VariableWL.ProductImages.Instance.rightForm line 39
  7. structure OAI.VariableWL.ProductImages.Instance.Witness line 42
  8. def OAI.VariableWL.ProductImages.Instance.Consistent line 49
  9. def OAI.VariableWL.ProductImages.Instance.Witness.wireValues line 54
  10. theorem OAI.VariableWL.ProductImages.Instance.Witness.wireValues_nonempty line 57
  11. theorem OAI.VariableWL.ProductImages.Instance.Witness.right_image line 60
  12. theorem OAI.VariableWL.ProductImages.Instance.Witness.lift_left line 64
  13. theorem OAI.VariableWL.ProductImages.Instance.Witness.lift_right line 67
  14. theorem OAI.VariableWL.ProductImages.Instance.exists_ambient line 75
  15. def OAI.VariableWL.ProductImages.Instance.ambient line 83
  16. theorem OAI.VariableWL.ProductImages.Instance.ambient_on_domain line 86
  17. def OAI.VariableWL.ProductImages.Instance.labels line 92
  18. def OAI.VariableWL.ProductImages.Instance.Matches line 96
  19. theorem OAI.VariableWL.ProductImages.Instance.matches_left line 99
  20. theorem OAI.VariableWL.ProductImages.Instance.matches_right line 106
  21. def OAI.VariableWL.ProductImages.Instance.alignment line 115
  22. theorem OAI.VariableWL.ProductImages.Instance.alignment_match line 120
  23. abbrev OAI.VariableWL.ProductImages.Instance.Shifts line 150
  24. def OAI.VariableWL.ProductImages.Instance.shiftLeft line 152
  25. def OAI.VariableWL.ProductImages.Instance.shiftRight line 156
  26. def OAI.VariableWL.ProductImages.Instance.ShiftSystem line 160
  27. def OAI.VariableWL.ProductImages.Instance.cutShifts line 163
  28. theorem OAI.VariableWL.ProductImages.Instance.cutShifts_equation line 167
  29. theorem OAI.VariableWL.ProductImages.Instance.small_shift_exists line 184
  30. theorem OAI.VariableWL.ProductImages.Instance.internal_equation line 192