OAI/Probability/LatticeSurface/Convexity/RadialExposure.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TriangularLipschitz.shell line 24
  2. def OAI.TriangularLipschitz.radialPoint line 26
  3. lemma OAI.TriangularLipschitz.mem_shell line 33
  4. lemma OAI.TriangularLipschitz.latticeDist_nonneg line 40
  5. lemma OAI.TriangularLipschitz.latticeDist_comm line 44
  6. lemma OAI.TriangularLipschitz.left_mem_box line 51
  7. lemma OAI.TriangularLipschitz.left_mem_shell_iff line 56
  8. lemma OAI.TriangularLipschitz.left_shell_distance line 61
  9. lemma OAI.TriangularLipschitz.other_face_distance line 71
  10. lemma OAI.TriangularLipschitz.left_compressed_distance line 82
  11. lemma OAI.TriangularLipschitz.left_opposite_distance line 90
  12. lemma OAI.TriangularLipschitz.left_radial_distance line 98
  13. lemma OAI.TriangularLipschitz.left_tangential_distance line 102
  14. def OAI.TriangularLipschitz.unitSign line 106
  15. lemma OAI.TriangularLipschitz.abs_unitSign line 108
  16. lemma OAI.TriangularLipschitz.compressed_slack line 112
  17. lemma OAI.TriangularLipschitz.far_plus_two_slack line 126
  18. lemma OAI.TriangularLipschitz.expose_left_compatible line 134
  19. lemma OAI.TriangularLipschitz.other_face_slack line 201
  20. lemma OAI.TriangularLipschitz.opposite_slack line 215
  21. lemma OAI.TriangularLipschitz.near_left_bounds line 225
  22. lemma OAI.TriangularLipschitz.far_left_bounds line 363
  23. lemma OAI.TriangularLipschitz.expose_left_radial line 404
  24. def OAI.TriangularLipschitz.boxSymmetry line 438
  25. lemma OAI.TriangularLipschitz.boxSymmetry_involutive line 445
  26. lemma OAI.TriangularLipschitz.boxSymmetry_injective line 451
  27. lemma OAI.TriangularLipschitz.boxSymmetry_mem_box line 455
  28. lemma OAI.TriangularLipschitz.boxSymmetry_mem_shell line 460
  29. lemma OAI.TriangularLipschitz.boxSymmetry_adj line 465
  30. lemma OAI.TriangularLipschitz.boxSymmetry_distance line 470
  31. lemma OAI.TriangularLipschitz.boxSymmetry_left_radial line 478
  32. lemma OAI.TriangularLipschitz.boxSymmetry_left_center line 482
  33. lemma OAI.TriangularLipschitz.boxSymmetry_left_neighbor line 486
  34. theorem OAI.TriangularLipschitz.triangular_radial_exposure line 490