OAI/Combinatorics/VariableWL/BlockImages.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.Blocks.dimension line 12
  2. abbrev OAI.VariableWL.Blocks.Value line 16
  3. def OAI.VariableWL.Blocks.vectorShift line 18
  4. def OAI.VariableWL.Blocks.linkLeft line 22
  5. def OAI.VariableWL.Blocks.linkRight line 30
  6. def OAI.VariableWL.Blocks.leftConstant line 38
  7. def OAI.VariableWL.Blocks.rightConstant line 39
  8. def OAI.VariableWL.Blocks.linkConstant line 41
  9. theorem OAI.VariableWL.Blocks.dependent_linear_apply line 43
  10. theorem OAI.VariableWL.Blocks.linkLeft_eval line 48
  11. theorem OAI.VariableWL.Blocks.linkRight_eval line 64
  12. theorem OAI.VariableWL.Blocks.link_equation_iff line 80
  13. abbrev OAI.VariableWL.Blocks.ReadoutValue line 94
  14. abbrev OAI.VariableWL.Blocks.Potentials line 98
  15. def OAI.VariableWL.Blocks.marker line 100
  16. def OAI.VariableWL.Blocks.potentialValues line 102
  17. theorem OAI.VariableWL.Blocks.potential_square line 109
  18. def OAI.VariableWL.Blocks.gaugePotentials line 128
  19. theorem OAI.VariableWL.Blocks.gauge_horizontal_readout line 131
  20. theorem OAI.VariableWL.Blocks.gauge_vertical_readout line 138
  21. theorem OAI.VariableWL.Markers.walkSum_copy line 155
  22. theorem OAI.VariableWL.Markers.exists_potential_all line 160
  23. theorem OAI.VariableWL.Wrapping.RowDiagram.nonwrapping_potential line 190
  24. theorem OAI.VariableWL.Blocks.readout_adj line 207
  25. theorem OAI.VariableWL.Blocks.diagram_mono line 212
  26. theorem OAI.VariableWL.Blocks.gauge_nonwrapping line 217
  27. def OAI.VariableWL.ProductImages.Instance.replaceInternal line 254
  28. theorem OAI.VariableWL.ProductImages.Instance.replaceInternal_agree_outside line 260
  29. theorem OAI.VariableWL.ProductImages.Instance.replaceInternal_system line 269
  30. theorem OAI.VariableWL.ProductImages.Instance.exists_scalar_shift line 295
  31. theorem OAI.VariableWL.ProductImages.Instance.internal_adj_values line 306
  32. theorem OAI.VariableWL.ProductImages.Instance.scalar_constant line 316
  33. theorem OAI.VariableWL.ProductImages.Instance.bool_perm_eq_of_apply line 346
  34. def OAI.VariableWL.ProductImages.Instance.transport line 356
  35. theorem OAI.VariableWL.ProductImages.Instance.alignment_link line 359
  36. def OAI.VariableWL.ProductImages.Instance.relativeAlignment line 373
  37. theorem OAI.VariableWL.ProductImages.Instance.relativeAlignment_link line 377
  38. theorem OAI.VariableWL.ProductImages.Instance.relativeAlignment_reachable line 385