OAI/GroupTheory/PolycyclicRecognition/Algebra/FactorExtensionTopology.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Completing the kernel while retaining the discrete quotient

  1. theorem OAI.PolycyclicRecognition.continuous_discrete_parameter line 13
  2. def OAI.PolycyclicRecognition.factorExtensionTopology line 31
  3. def OAI.PolycyclicRecognition.factorExtensionHomeomorph line 36
  4. theorem OAI.PolycyclicRecognition.continuous_factor_left line 41
  5. theorem OAI.PolycyclicRecognition.continuous_factor_right line 44
  6. theorem OAI.PolycyclicRecognition.continuous_factor_inl line 47
  7. instance OAI.PolycyclicRecognition.(instance at line 50) line 50
  8. instance OAI.PolycyclicRecognition.(instance at line 53) line 53
  9. theorem OAI.PolycyclicRecognition.factorExtensionTopologicalGroup line 60

    Source documentation

    Individual continuous kernel automorphisms suffice over a discrete quotient.

    theorem factorExtensionTopologicalGroup (ha : ∀ q, Continuous (S.action q)) :
    IsTopologicalGroup (FactorExtension S) := by
…

    Mentions: OAI.PolycyclicRecognition.FactorExtension