OAI/GroupTheory/PolycyclicRecognition/Geometry/FlowNeighborhoods.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Connected neighborhoods admit one time interval for finitely many flows

  1. theorem OAI.PolycyclicRecognition.flowLineBase_rescale line 19
  2. theorem OAI.PolycyclicRecognition.exists_connected_flow_neighborhood line 33