OAI/GroupTheory/PolycyclicRecognition/Algebra/SeparateConnectedGeneration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Connected generation with separately continuous operations

Two points in the image of a separately continuous two-variable map are joined by two intersecting connected slices. A connected set containing the identity then generates a connected subgroup, by taking the identity component inside the generated subgroup itself.

  1. theorem OAI.PolycyclicRecognition.isPreconnected_image2_separate line 16
  2. theorem OAI.PolycyclicRecognition.isPreconnected_subgroup_closure line 35