OAI/Combinatorics/VariableWL/BlockCoordinates.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VariableWL.Subdivision.realFree_reachable_wire line 10
  2. theorem OAI.VariableWL.Markers.walkSum_mapLe line 37
  3. theorem OAI.VariableWL.Markers.exists_nonzero_edge line 43
  4. def OAI.VariableWL.Blocks.anchor line 59
  5. theorem OAI.VariableWL.Blocks.readout_reachable line 63
  6. theorem OAI.VariableWL.Blocks.wrapping_mono line 84
  7. theorem OAI.VariableWL.Blocks.wrapping_connected line 91
  8. theorem OAI.VariableWL.ProductImages.Instance.lift_scalar_to_cut line 133
  9. theorem OAI.VariableWL.ProductImages.Instance.agree_from_real line 167
  10. theorem OAI.VariableWL.ProductImages.Instance.agree_from_internal line 179
  11. def OAI.VariableWL.Blocks.componentBlocks line 192
  12. theorem OAI.VariableWL.Blocks.mem_componentBlocks line 198
  13. theorem OAI.VariableWL.Blocks.componentBlocks_subset line 205
  14. theorem OAI.VariableWL.Blocks.readout_component line 211
  15. theorem OAI.VariableWL.Blocks.component_adj line 221
  16. theorem OAI.VariableWL.Blocks.component_reachable line 234
  17. theorem OAI.VariableWL.Blocks.component_anchors_connected line 246
  18. theorem OAI.VariableWL.Subdivision.internal_reachable_invariant line 261
  19. theorem OAI.VariableWL.ProductImages.Instance.alignment_internal_adj line 291
  20. theorem OAI.VariableWL.ProductImages.Instance.alignment_internal_reachable line 307
  21. def OAI.VariableWL.Blocks.typesOf line 320
  22. def OAI.VariableWL.Blocks.supportTypes line 326
  23. theorem OAI.VariableWL.Blocks.type_has_horizontal line 330
  24. theorem OAI.VariableWL.Blocks.anchor_mem_types line 344
  25. theorem OAI.VariableWL.Blocks.supportLinks_endpoints line 348
  26. theorem OAI.VariableWL.Blocks.support_reachable_mem line 361
  27. theorem OAI.VariableWL.Blocks.support_types_connected line 374
  28. def OAI.VariableWL.Blocks.addressAt line 388
  29. def OAI.VariableWL.Blocks.Recovers line 391
  30. theorem OAI.VariableWL.Blocks.anchor_label_allowed line 396
  31. theorem OAI.VariableWL.Blocks.firstLabel_anchor line 403
  32. theorem OAI.VariableWL.Blocks.recovers_unique line 413
  33. theorem OAI.VariableWL.Blocks.wrapping_address_allowed line 425
  34. theorem OAI.VariableWL.Blocks.permutation_coordinates line 459
  35. theorem OAI.VariableWL.Blocks.addressAt_cut_independent line 466
  36. theorem OAI.VariableWL.Blocks.recovered_overlap line 489
  37. theorem OAI.VariableWL.ProductImages.Instance.scalar_image_of_real line 509