OAI/Combinatorics/Progressions/Nilpotent/RealifiedBCHFiniteAtlas.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieBCHGroup.quotientCoordinateChart line 24
  2. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotientCoordinateChart_apply line 40
  3. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotientCoordinateChart_source line 44
  4. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotientCoordinateChart_target line 48
  5. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotientCoordinateChart_center_mem line 53
  6. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotient_covered_by_coordinate_box line 77
  7. theorem OAI.Erdos3.exists_realification_metric_partition_exp_bound line 96
  8. def OAI.Erdos3.NilpotentLieBCHGroup.quotientChartedSpace line 166
  9. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotientChartedSpace_chartAt line 174
  10. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotientCoordinateChart_mem_atlas line 178
  11. theorem OAI.Erdos3.NilpotentLieBCHGroup.isManifold_quotient line 183
  12. theorem OAI.Erdos3.NilpotentLieBCHGroup.contMDiff_quotient_mk line 200
  13. theorem OAI.Erdos3.exists_realification_open_charts_exp_bound line 232
  14. theorem OAI.Erdos3.NilpotentLieBCHGroup.inv_mul_coordinates_bound line 279
  15. theorem OAI.Erdos3.NilpotentLieBCHGroup.finite_quotient_coordinate_cover line 295
  16. theorem OAI.Erdos3.NilpotentLieBCHGroup.finite_quotient_coordinate_chart_cover line 353
  17. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotient_chart_transition_mem_contDiffGroupoid line 397
  18. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotient_chart_mem_maximalAtlas line 410
  19. theorem OAI.Erdos3.exists_bch_chart_cover_exp_bound line 443
  20. theorem OAI.Erdos3.half_radius_inverse_power_bound line 502
  21. theorem OAI.Erdos3.shifted_center_power_bound line 514
  22. theorem OAI.Erdos3.exists_bch_flexible_cover_exp_bound line 521
  23. theorem OAI.Erdos3.exists_realification_finite_atlas_exp_bound line 561