OAI/NumberTheory/PrimePackets/ConditionalFibers.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.fst_map_fibers_of_measurable line 117
  2. lemma OAI.PrimeDegreePackets.compProd_map_fibers_leftInverse line 125
  3. lemma OAI.PrimeDegreePackets.conditional_map_fibers_leftInverse line 141
  4. theorem OAI.PrimeDegreePackets.conditional_map_fibers_embedding line 160
  5. abbrev OAI.PrimeDegreePackets.baseSubtypeMap line 177
  6. lemma OAI.PrimeDegreePackets.baseSubtypeMap_embedding line 179
  7. lemma OAI.PrimeDegreePackets.baseSubtypeMap_range line 184
  8. lemma OAI.PrimeDegreePackets.map_comap_baseSubtype line 192
  9. lemma OAI.PrimeDegreePackets.fst_map_comap_baseSubtype line 196
  10. theorem OAI.PrimeDegreePackets.conditional_comap_baseSubtype line 205
  11. lemma OAI.PrimeDegreePackets.rootSliceOverlap_isOpen line 230
  12. abbrev OAI.PrimeDegreePackets.rootOverlapParam line 240
  13. abbrev OAI.PrimeDegreePackets.RootBox.overlapDomain line 245
  14. def OAI.PrimeDegreePackets.RootBox.overlapMeasure line 249
  15. instance OAI.PrimeDegreePackets.RootBox.overlapMeasure_finite line 253
  16. lemma OAI.PrimeDegreePackets.RootBox.overlapDomain_open line 258
  17. lemma OAI.PrimeDegreePackets.RootBox.overlapMeasure_apply line 263
  18. lemma OAI.PrimeDegreePackets.RootBox.overlapMeasure_conditional line 278
  19. theorem OAI.PrimeDegreePackets.RootBox.overlapMeasure_transition line 286
  20. lemma OAI.PrimeDegreePackets.conditional_restrict_normalized line 317
  21. theorem OAI.PrimeDegreePackets.conditional_overlap_normalized line 340
  22. theorem OAI.PrimeDegreePackets.RootBox.overlap_conditional_projective line 373
  23. lemma OAI.PrimeDegreePackets.fst_restrict_base line 418
  24. abbrev OAI.PrimeDegreePackets.RootBox.transitionOverlapMeasure line 426
  25. lemma OAI.PrimeDegreePackets.RootBox.transitionOverlapMeasure_apply line 431
  26. lemma OAI.PrimeDegreePackets.RootBox.transitionOverlapMeasure_restrict_le line 441
  27. lemma OAI.PrimeDegreePackets.RootBox.transition_base_ae_of_ae line 463
  28. lemma OAI.PrimeDegreePackets.RootBox.transition_base_ae_source line 481
  29. lemma OAI.PrimeDegreePackets.RootBox.transition_base_ae_target line 492
  30. lemma OAI.PrimeDegreePackets.anchorNormalize_map line 521
  31. lemma OAI.PrimeDegreePackets.anchorNormalize_congr_restriction line 528
  32. lemma OAI.PrimeDegreePackets.anchorNormalize_reanchor_map line 535
  33. theorem OAI.PrimeDegreePackets.projective_extensions_overlap line 550