OAI/GroupTheory/SimpleAmenable/Amenability/BarrierLineGeometry.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.barrierLinePoint line 18
  2. def OAI.SimpleAmenable.barrierLineParameter line 22
  3. def OAI.SimpleAmenable.barrierLineLower line 25
  4. def OAI.SimpleAmenable.barrierLineUpper line 28
  5. theorem OAI.SimpleAmenable.cutForm_barrierLinePoint line 31
  6. theorem OAI.SimpleAmenable.barrierLineParameter_point line 35
  7. theorem OAI.SimpleAmenable.barrierLinePoint_parameter line 39
  8. def OAI.SimpleAmenable.barrierCandidate line 44
  9. theorem OAI.SimpleAmenable.squareInterior_cutForm_bound line 47
  10. theorem OAI.SimpleAmenable.barrierCandidate_finite line 54
  11. theorem OAI.SimpleAmenable.barrierCandidate_coordinate line 65
  12. theorem OAI.SimpleAmenable.barrierLinePoint_interior_iff line 74
  13. def OAI.SimpleAmenable.barrierTangent line 95
  14. theorem OAI.SimpleAmenable.barrierLinePoint_sub line 98
  15. theorem OAI.SimpleAmenable.barrierTangent_cut line 102
  16. theorem OAI.SimpleAmenable.positiveDiagonal_transverse line 105
  17. theorem OAI.SimpleAmenable.exists_barrierFlagDirection line 110
  18. def OAI.SimpleAmenable.barrierFlagDirection line 132
  19. theorem OAI.SimpleAmenable.barrierFlagDirection_spec line 135
  20. def OAI.SimpleAmenable.barrierIncoming line 148
  21. theorem OAI.SimpleAmenable.barrierLineLower_lt_upper line 151
  22. theorem OAI.SimpleAmenable.barrierIncoming_bounds line 159
  23. theorem OAI.SimpleAmenable.barrierIncoming_boundary line 205
  24. theorem OAI.SimpleAmenable.barrierIncoming_edge line 214
  25. theorem OAI.SimpleAmenable.barrierIncoming_lattice line 237
  26. def OAI.SimpleAmenable.barrierIncomingSite line 247