OAI/Probability/LatticeSurface/Geometry/StrictFilling.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictFilling.clip line 7
  2. lemma OAI.StrictFilling.clip_eq_self line 9
  3. lemma OAI.StrictFilling.clip_same line 13
  4. lemma OAI.StrictFilling.clip_between_zero line 16
  5. def OAI.StrictFilling.medianZero line 24
  6. lemma OAI.StrictFilling.medianZero_properties line 26
  7. lemma OAI.StrictFilling.lipschitz_add_const line 42
  8. lemma OAI.StrictFilling.lipschitz_const_sub line 49
  9. lemma OAI.StrictFilling.lipschitz_clip line 53
  10. lemma OAI.StrictFilling.endpoint_lower line 59
  11. lemma OAI.StrictFilling.endpoint_upper line 73
  12. lemma OAI.StrictFilling.cone_preserves_interval line 87
  13. def OAI.StrictFilling.twoRadius line 92
  14. def OAI.StrictFilling.twoClip line 94
  15. lemma OAI.StrictFilling.twoRadius_lipschitz line 97
  16. lemma OAI.StrictFilling.twoClip_lipschitz line 102
  17. lemma OAI.StrictFilling.twoClip_between_zero line 106
  18. lemma OAI.StrictFilling.twoClip_endpoints line 117
  19. lemma OAI.StrictFilling.cone_eq_self_of_dist line 122
  20. lemma OAI.StrictFilling.twoClip_eq_self line 127
  21. lemma OAI.StrictFilling.pin_compatible line 134
  22. lemma OAI.StrictFilling.room_compatible line 145
  23. theorem OAI.StrictFilling.strict_filling_movable_first line 155
  24. theorem OAI.StrictFilling.strict_filling line 232
  25. abbrev OAI.StrictFilling.Component line 255
  26. instance OAI.StrictFilling.componentMetric line 257
  27. lemma OAI.StrictFilling.edge_bound_walk line 269
  28. lemma OAI.StrictFilling.edge_bound_dist line 280
  29. lemma OAI.StrictFilling.component_lipschitz line 286
  30. lemma OAI.StrictFilling.component_separated line 293
  31. theorem OAI.StrictFilling.graph_strict_filling line 299