OAI/Combinatorics/Hamiltonian/DiskRegions.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Connected face regions and the exact disk Euler formula.

  1. def OAI.Barnette.Network.regionEdges line 13
  2. lemma OAI.Barnette.Network.mem_regionEdges line 17
  3. def OAI.Barnette.Network.regionVertices line 21
  4. lemma OAI.Barnette.Network.mem_regionVertices line 25
  5. def OAI.Barnette.Network.region line 29
  6. lemma OAI.Barnette.Network.region_map line 34
  7. lemma OAI.Barnette.Network.region_boundary line 38
  8. lemma OAI.Barnette.Network.push_subtype_apply line 44
  9. lemma OAI.Barnette.Network.push_subtype_outside line 50
  10. lemma OAI.Barnette.Network.extend_gradient_outside line 55
  11. lemma OAI.Barnette.Network.extend_restrict_gradient line 62
  12. lemma OAI.Barnette.Network.region_connected line 74
  13. def OAI.Barnette.Network.regionCycleMap line 162
  14. lemma OAI.Barnette.Network.regionCycleMap_injective line 167
  15. lemma OAI.Barnette.Network.region_cycles_eq_range line 185
  16. lemma OAI.Barnette.Network.region_dim_cycles line 241
  17. theorem OAI.Barnette.Network.region_euler line 252
  18. lemma OAI.Barnette.Network.sum_stars line 270
  19. lemma OAI.Barnette.Network.cubic_region_count line 290
  20. lemma OAI.Barnette.Network.disk_euler_count line 305