OAI/Geometry/NilpotentCharts/CentralSubspaces.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Closed central subspaces and rationality of the final lower-central layer.

  1. lemma OAI.RawLieIntegration.subspaceAxes_central_inclusion line 21
  2. def OAI.RawLieIntegration.centralSubspaceHom line 36
  3. lemma OAI.RawLieIntegration.centralSubspaceHom_apply line 40
  4. lemma OAI.RawLieIntegration.centralSubspaceHom_le_center line 44
  5. lemma OAI.RawLieIntegration.centralSubspaceAxes_closedEmbedding line 48
  6. lemma OAI.RawLieIntegration.centralSubspace_range_membership line 64
  7. lemma OAI.RawLieIntegration.centralSubspace_range_closed line 72
  8. instance OAI.RawLieIntegration.centralSubspace_range_normal line 80
  9. lemma OAI.RawLieIntegration.last_lowerCentral_le_center line 96
  10. theorem OAI.RawLieIntegration.last_central_rational_subspace line 110