OAI/Geometry/Cannon/PlaneTopology/HalfParam.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CannonEmbeddedArc.Arc.extend_star_in_sector line 53
  2. theorem OAI.CannonEmbeddedArc.Arc.finite_prescribed_star line 169
  3. def OAI.CannonEmbeddedArc.Arc.halfParam line 220
  4. lemma OAI.CannonEmbeddedArc.Arc.zero_lt_halfParam line 221
  5. lemma OAI.CannonEmbeddedArc.Arc.halfParam_lt_one line 222
  6. def OAI.CannonEmbeddedArc.Arc.bisect line 224
  7. def OAI.CannonEmbeddedArc.Arc.bisectParam line 228
  8. lemma OAI.CannonEmbeddedArc.Arc.bisect_apply line 232
  9. lemma OAI.CannonEmbeddedArc.Arc.bisect_param_endpoint line 234
  10. lemma OAI.CannonEmbeddedArc.Arc.bisect_false_ne_one line 239
  11. lemma OAI.CannonEmbeddedArc.Arc.bisect_true_ne_zero line 241
  12. lemma OAI.CannonEmbeddedArc.Arc.bisect_same_param line 243
  13. lemma OAI.CannonEmbeddedArc.Arc.bisect_compatible line 252
  14. lemma OAI.CannonEmbeddedArc.Arc.bisect_range line 262
  15. lemma OAI.CannonEmbeddedArc.Arc.weak_compatible_bisect line 283
  16. theorem OAI.CannonEmbeddedArc.Arc.bisected_weak_family line 302
  17. lemma OAI.CannonEmbeddedArc.Arc.bisected_family_range line 316
  18. lemma OAI.CannonEmbeddedArc.Arc.finiteSupport_bisect line 329
  19. lemma OAI.CannonEmbeddedArc.Arc.tame_initial_window line 341
  20. def OAI.CannonEmbeddedArc.Arc.transverse line 366
  21. lemma OAI.CannonEmbeddedArc.Arc.transverse_apply line 368
  22. lemma OAI.CannonEmbeddedArc.Arc.transverse_self line 369
  23. lemma OAI.CannonEmbeddedArc.Arc.transverse_surjective line 373
  24. lemma OAI.CannonEmbeddedArc.Arc.transverse_segment line 379
  25. lemma OAI.CannonEmbeddedArc.Arc.tame_endpoint_transverse line 385
  26. theorem OAI.CannonEmbeddedArc.Arc.tame_vertex_lines line 399
  27. def OAI.CannonSectors.sector line 442
  28. lemma OAI.CannonSectors.sector_open line 445
  29. lemma OAI.CannonSectors.sector_convex line 454
  30. lemma OAI.CannonSectors.sector_radial line 476
  31. lemma OAI.CannonSectors.radial_vertex_closure line 486
  32. lemma OAI.CannonSectors.sector_vertex_closure line 500
  33. lemma OAI.CannonSectors.sector_in_complement line 504
  34. lemma OAI.CannonSectors.transverse_complement_dense line 512
  35. lemma OAI.CannonSectors.mem_some_sector line 522
  36. theorem OAI.CannonSectors.face_contains_sector line 532