OAI/Combinatorics/HoneycombCorridor/Incidence.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.extendOn line 11
  2. theorem OAI.PolynomialVacuumBridge.Corridor.extendOn_apply_mem line 15
  3. theorem OAI.PolynomialVacuumBridge.Corridor.extendOn_apply_not_mem line 19
  4. theorem OAI.PolynomialVacuumBridge.Corridor.extendOn_support line 23
  5. theorem OAI.PolynomialVacuumBridge.Corridor.extendOn_injective line 29
  6. theorem OAI.PolynomialVacuumBridge.Corridor.extendOn_restrict line 36
  7. def OAI.PolynomialVacuumBridge.Corridor.rationalBoundary line 45
  8. theorem OAI.PolynomialVacuumBridge.Corridor.rationalBoundary_single line 48
  9. theorem OAI.PolynomialVacuumBridge.Corridor.rationalBoundary_up line 53
  10. theorem OAI.PolynomialVacuumBridge.Corridor.rationalBoundary_down line 64
  11. theorem OAI.PolynomialVacuumBridge.Corridor.rationalBoundary_apply line 78
  12. theorem OAI.PolynomialVacuumBridge.Corridor.rationalBoundary_eq_zero line 83
  13. def OAI.PolynomialVacuumBridge.Corridor.incidenceMatrix line 87
  14. theorem OAI.PolynomialVacuumBridge.Corridor.cell_upEnd line 91
  15. theorem OAI.PolynomialVacuumBridge.Corridor.cell_downEnd line 99
  16. theorem OAI.PolynomialVacuumBridge.Corridor.transpose_incidence_apply line 107
  17. theorem OAI.PolynomialVacuumBridge.Corridor.extendOn_add line 128
  18. theorem OAI.PolynomialVacuumBridge.Corridor.extendOn_smul line 133
  19. theorem OAI.PolynomialVacuumBridge.Corridor.extendOn_eq_sum line 138
  20. theorem OAI.PolynomialVacuumBridge.Corridor.incidence_apply line 156
  21. theorem OAI.PolynomialVacuumBridge.Corridor.rationalBoundary_support_cells line 166
  22. theorem OAI.PolynomialVacuumBridge.Corridor.incidence_zero_iff line 179
  23. theorem OAI.PolynomialVacuumBridge.Corridor.gradient_zero_off_cells line 197
  24. def OAI.PolynomialVacuumBridge.Corridor.cellFaceBoundary line 206
  25. theorem OAI.PolynomialVacuumBridge.Corridor.extend_faceBoundary line 218
  26. theorem OAI.PolynomialVacuumBridge.Corridor.cellFaceBoundary_injective line 227
  27. theorem OAI.PolynomialVacuumBridge.Corridor.cellFaceBoundary_range line 234
  28. theorem OAI.PolynomialVacuumBridge.Corridor.represented_nonzero_edge_mem line 258
  29. theorem OAI.PolynomialVacuumBridge.Corridor.contour_outgoing_nonzero line 271
  30. theorem OAI.PolynomialVacuumBridge.Corridor.contour_step_mem line 279
  31. theorem OAI.PolynomialVacuumBridge.Corridor.contour_flat_trace line 285
  32. theorem OAI.PolynomialVacuumBridge.Corridor.cycle_vertices_nonempty line 304
  33. theorem OAI.PolynomialVacuumBridge.Corridor.transpose_incidence_kernel line 312
  34. theorem OAI.PolynomialVacuumBridge.Corridor.simple_cycle_cell_euler line 361