OAI/Combinatorics/VariableWL/PortGraph.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.VariableWL.SubcubicRealization.PortGraph line 10
  2. def OAI.VariableWL.SubcubicRealization.PortGraph.graph line 16
  3. structure OAI.VariableWL.SubcubicRealization.Vertex line 21
  4. def OAI.VariableWL.SubcubicRealization.Vertex.triangle line 30
  5. def OAI.VariableWL.SubcubicRealization.Vertex.connector line 31
  6. def OAI.VariableWL.SubcubicRealization.Vertex.equivSigma line 33
  7. instance OAI.VariableWL.SubcubicRealization.Vertex.(instance at line 39) line 39
  8. def OAI.VariableWL.SubcubicRealization.Internal line 46
  9. def OAI.VariableWL.SubcubicRealization.External line 51
  10. def OAI.VariableWL.SubcubicRealization.graph line 54
  11. theorem OAI.VariableWL.SubcubicRealization.adjacency_owner line 69
  12. theorem OAI.VariableWL.SubcubicRealization.triangle_adj_triangle line 75
  13. theorem OAI.VariableWL.SubcubicRealization.triangle_adj line 79
  14. theorem OAI.VariableWL.SubcubicRealization.triangle_characterization line 96
  15. def OAI.VariableWL.SubcubicRealization.neighborSlot line 157
  16. theorem OAI.VariableWL.SubcubicRealization.internal_of_nontriangle line 162
  17. theorem OAI.VariableWL.SubcubicRealization.neighborSlot_injective line 169
  18. theorem OAI.VariableWL.SubcubicRealization.degree_le_three line 206
  19. theorem OAI.VariableWL.SubcubicRealization.triangle_degree line 211
  20. theorem OAI.VariableWL.SubcubicRealization.high_adj line 240
  21. theorem OAI.VariableWL.SubcubicRealization.high_degree_le_two line 250
  22. theorem OAI.VariableWL.SubcubicRealization.terminal_degree line 267
  23. theorem OAI.VariableWL.SubcubicRealization.intermediate_degree line 283
  24. theorem OAI.VariableWL.SubcubicRealization.connector_used_degree line 300
  25. theorem OAI.VariableWL.SubcubicRealization.same_owner_reachable line 317
  26. theorem OAI.VariableWL.SubcubicRealization.underlying_edge_reachable line 335
  27. theorem OAI.VariableWL.SubcubicRealization.connected line 342
  28. def OAI.VariableWL.SubcubicRealization.vertexEquiv line 361
  29. theorem OAI.VariableWL.SubcubicRealization.vertexEquiv_internal line 369
  30. theorem OAI.VariableWL.SubcubicRealization.vertexEquiv_adj line 379