OAI/Combinatorics/Progressions/Nilpotent/BCHChartCutoffSmooth.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Erdos3.NilpotentLieBCHGroup.(instance at line 20) line 20
  2. theorem OAI.Erdos3.NilpotentLieBCHGroup.continuous_coord line 24
  3. theorem OAI.Erdos3.NilpotentLieBCHGroup.continuous_mk line 28
  4. def OAI.Erdos3.NilpotentLieBCHGroup.coordHomeomorph line 31
  5. instance OAI.Erdos3.NilpotentLieBCHGroup.(instance at line 39) line 39
  6. instance OAI.Erdos3.NilpotentLieBCHGroup.(instance at line 42) line 42
  7. theorem OAI.Erdos3.NilpotentLieBCHGroup.isTopologicalGroup_of_continuous_lie line 45
  8. theorem OAI.Erdos3.NilpotentLieBCHGroup.continuous_map_of_continuous line 69
  9. instance OAI.Erdos3.NilpotentLieBCHGroup.(instance at line 80) line 80
  10. theorem OAI.Erdos3.NilpotentLieBCHGroup.connected_simplyConnected line 88
  11. def OAI.Erdos3.NilpotentLieBCHGroup.basisHomeomorph line 109
  12. theorem OAI.Erdos3.NilpotentLieBCHGroup.basisHomeomorph_apply line 114
  13. theorem OAI.Erdos3.NilpotentLieBCHGroup.closed_discrete_subgroup_of_grid line 117
  14. theorem OAI.Erdos3.NilpotentLieBCHGroup.discreteTopology_subgroup_of_grid line 131
  15. def OAI.Erdos3.realLieSubalgebraOverRat line 147
  16. def OAI.Erdos3.NilpotentLieBCHGroup.realLieSubgroup line 154
  17. theorem OAI.Erdos3.NilpotentLieBCHGroup.mem_realLieSubgroup line 157
  18. def OAI.Erdos3.NilpotentLieBCHGroup.realLieSubgroupCoordHomeomorph line 162
  19. theorem OAI.Erdos3.NilpotentLieBCHGroup.realLieSubgroup_contractible line 173
  20. theorem OAI.Erdos3.NilpotentLieBCHGroup.realLieSubgroup_connected_simplyConnected line 177
  21. theorem OAI.Erdos3.NilpotentLieBCHGroup.realLieSubgroup_closed line 183
  22. def OAI.Erdos3.NilpotentLieBCHGroup.coordinateBox line 201
  23. theorem OAI.Erdos3.NilpotentLieBCHGroup.isCompact_coordinateBox line 206
  24. def OAI.Erdos3.NilpotentLieBCHGroup.basisChartedSpace line 241
  25. theorem OAI.Erdos3.NilpotentLieBCHGroup.isManifold_basis line 247
  26. theorem OAI.Erdos3.NilpotentLieBCHGroup.contMDiff_basisHomeomorph line 252
  27. theorem OAI.Erdos3.NilpotentLieBCHGroup.contMDiff_basisHomeomorph_symm line 257
  28. def OAI.Erdos3.NilpotentLieBCHGroup.basisDiffeomorph line 267
  29. theorem OAI.Erdos3.NilpotentLieBCHGroup.lieGroup_basis line 278
  30. theorem OAI.Erdos3.realification_layer_reduction_in_cell line 331
  31. theorem OAI.Erdos3.exists_realification_layer_reduction line 375
  32. theorem OAI.Erdos3.NilpotentLieBCHGroup.realificationHom_coordinates line 402
  33. theorem OAI.Erdos3.NilpotentLieBCHGroup.realification_subgroup_grid line 407
  34. theorem OAI.Erdos3.NilpotentLieBCHGroup.realification_subgroup_closed_discrete line 422
  35. theorem OAI.Erdos3.NilpotentLieFiltration.rational_inclusion_mem_realLayer_iff line 445
  36. theorem OAI.Erdos3.NilpotentLieFiltration.realificationHom_mem_subgroup_iff line 449
  37. theorem OAI.Erdos3.NilpotentLieFiltration.realification_subgroup_eq_realLieSubgroup line 453
  38. theorem OAI.Erdos3.NilpotentLieFiltration.realification_subgroup_contractible line 460
  39. theorem OAI.Erdos3.NilpotentLieFiltration.realification_subgroup_connected_simplyConnected line 464
  40. theorem OAI.Erdos3.NilpotentLieFiltration.realification_subgroup_closed line 468
  41. theorem OAI.Erdos3.NilpotentLieBCHGroup.eventuallyEq_quotient_chartInverse line 489
  42. theorem OAI.Erdos3.NilpotentLieBCHGroup.contMDiffAt_quotient_chartInverse line 524
  43. theorem OAI.Erdos3.NilpotentLieBCHGroup.contDiffOn_quotient_chart_transition line 541
  44. theorem OAI.Erdos3.exists_realification_topology_of_grid line 575
  45. theorem OAI.Erdos3.NilpotentLieBCHGroup.contMDiff_quotient_chartCutoff line 615