OAI/GroupTheory/SimpleAmenable/Amenability/BarrierSignalSystem.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SimpleAmenable.BarrierSignalSystem line 15
  2. theorem OAI.SimpleAmenable.exists_barrierSignalSystem line 34
  3. theorem OAI.SimpleAmenable.BarrierSignalSystem.R₁_pos line 55
  4. theorem OAI.SimpleAmenable.BarrierSignalSystem.incoming_first_true line 57
  5. def OAI.SimpleAmenable.BarrierSignalSystem.marks line 67
  6. theorem OAI.SimpleAmenable.BarrierSignalSystem.mem_marks_iff line 71
  7. theorem OAI.SimpleAmenable.BarrierSignalSystem.intersection_first_true line 77
  8. theorem OAI.SimpleAmenable.BarrierSignalSystem.central_line_barrier line 92
  9. def OAI.SimpleAmenable.subdivisionBarrier line 123
  10. theorem OAI.SimpleAmenable.consecutiveSubdivision_local line 126
  11. theorem OAI.SimpleAmenable.consecutiveSubdivision_translate line 137
  12. theorem OAI.SimpleAmenable.subdivisionBarrier_translate_iff line 152
  13. theorem OAI.SimpleAmenable.mem_barrierActiveIntervals_image_iff line 178