OAI/NumberTheory/PrimePackets/LeafTransitions.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.RootBox.transition_source_fiber line 116
  2. lemma OAI.PrimeDegreePackets.RootBox.transition_target_fiber line 125
  3. theorem OAI.PrimeDegreePackets.RootBox.overlap_conditional_projective_explicit line 146
  4. lemma OAI.PrimeDegreePackets.RootBox.ae_leafMeasure_restrict_conditional line 166
  5. theorem OAI.PrimeDegreePackets.RootBox.ae_leafTransition_restrict line 184
  6. lemma OAI.PrimeDegreePackets.translated_window_chain_cover line 227
  7. theorem OAI.PrimeDegreePackets.RootBox.ae_leafTransition line 245
  8. theorem OAI.PrimeDegreePackets.RootBox.ae_leafTransition_anchor_mass line 309
  9. theorem OAI.PrimeDegreePackets.RootBox.ae_basedLeaf_transition line 340
  10. lemma OAI.PrimeDegreePackets.rootGroupParametrization_injective line 366
  11. theorem OAI.PrimeDegreePackets.exists_rootTransition_of_quotient_eq line 373
  12. lemma OAI.PrimeDegreePackets.RootBox.map_transitionOverlapMeasure line 401
  13. lemma OAI.PrimeDegreePackets.RootBox.ae_basedLeaf_lift_transition line 421
  14. theorem OAI.PrimeDegreePackets.RootBox.ae_basedLeaf_chart_compatibility line 456
  15. structure OAI.PrimeDegreePackets.BoundedRootBox line 486
  16. def OAI.PrimeDegreePackets.RootBox.coordinates line 497
  17. lemma OAI.PrimeDegreePackets.RootBox.param_coordinates line 500
  18. lemma OAI.PrimeDegreePackets.RootBox.coordinates_param line 504
  19. lemma OAI.PrimeDegreePackets.RootBox.aemeasurable_of_coordinate line 508
  20. lemma OAI.PrimeDegreePackets.RootBox.ae_of_coordinate line 518
  21. lemma OAI.PrimeDegreePackets.exists_boundedRootBox_at line 529
  22. lemma OAI.PrimeDegreePackets.exists_countable_boundedRootBox_cover line 544
  23. def OAI.PrimeDegreePackets.boundedRootAtlas line 555
  24. lemma OAI.PrimeDegreePackets.boundedRootAtlas_countable line 558
  25. lemma OAI.PrimeDegreePackets.boundedRootAtlas_covers line 561