OAI/Combinatorics/Hamiltonian/Traces.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Compact connected arc traces and uniform positive thickenings.

  1. def OAI.Barnette.PlaneEmbedding.curve line 13
  2. theorem OAI.Barnette.PlaneEmbedding.curve_zero line 16
  3. theorem OAI.Barnette.PlaneEmbedding.curve_one line 19
  4. theorem OAI.Barnette.PlaneEmbedding.curve_injective line 22
  5. theorem OAI.Barnette.PlaneEmbedding.curve_symm line 25
  6. theorem OAI.Barnette.PlaneEmbedding.curve_eq_point_iff line 31
  7. theorem OAI.Barnette.PlaneEmbedding.curve_eq_curve_interior line 37
  8. def OAI.Barnette.PlaneEmbedding.third line 45
  9. def OAI.Barnette.PlaneEmbedding.twoThirds line 46
  10. def OAI.Barnette.PlaneEmbedding.trace line 48
  11. theorem OAI.Barnette.PlaneEmbedding.trace_compact line 51
  12. theorem OAI.Barnette.PlaneEmbedding.trace_preconnected line 55
  13. def OAI.Barnette.PlaneEmbedding.branch line 59
  14. def OAI.Barnette.PlaneEmbedding.core line 62
  15. theorem OAI.Barnette.PlaneEmbedding.branch_point line 64
  16. theorem OAI.Barnette.PlaneEmbedding.branch_compact line 67
  17. theorem OAI.Barnette.PlaneEmbedding.core_compact line 73
  18. theorem OAI.Barnette.PlaneEmbedding.core_preconnected line 75
  19. theorem OAI.Barnette.PlaneEmbedding.initial_meeting line 78
  20. theorem OAI.Barnette.PlaneEmbedding.branch_disjoint line 103
  21. theorem OAI.Barnette.PlaneEmbedding.middle_nonendpoint line 127
  22. theorem OAI.Barnette.PlaneEmbedding.core_avoids_vertices line 139
  23. theorem OAI.Barnette.PlaneEmbedding.core_disjoint line 146
  24. theorem OAI.Barnette.PlaneEmbedding.branch_core_disjoint line 156
  25. theorem OAI.Barnette.PlaneEmbedding.branch_preconnected line 181
  26. theorem OAI.Barnette.PlaneEmbedding.branch_connected line 194
  27. theorem OAI.Barnette.PlaneEmbedding.third_le_twoThirds line 197
  28. theorem OAI.Barnette.PlaneEmbedding.symm_third line 201
  29. theorem OAI.Barnette.PlaneEmbedding.core_connected line 206
  30. theorem OAI.Barnette.PlaneEmbedding.branch_core_meets line 210
  31. theorem OAI.Barnette.PlaneEmbedding.finite_positive_radius line 223
  32. theorem OAI.Barnette.PlaneEmbedding.uniform_thickening line 240