OAI/Combinatorics/BalancedRyser/Deletion/DeletionFieldTransport.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.FieldTransport.pointEquiv line 12
  2. def OAI.Balanced.FieldTransport.directionEquiv line 15
  3. def OAI.Balanced.FieldTransport.lineEquiv line 18
  4. theorem OAI.Balanced.FieldTransport.lineEquiv_fst line 21
  5. theorem OAI.Balanced.FieldTransport.lineEquiv_snd line 24
  6. theorem OAI.Balanced.FieldTransport.lineEval_transport line 27
  7. theorem OAI.Balanced.FieldTransport.onLine_transport line 31
  8. def OAI.Balanced.FieldTransport.mapLines line 37
  9. def OAI.Balanced.FieldTransport.mapPoints line 40
  10. theorem OAI.Balanced.FieldTransport.card_mapLines line 44
  11. theorem OAI.Balanced.FieldTransport.card_mapPoints line 48
  12. theorem OAI.Balanced.FieldTransport.mem_mapLines line 52
  13. theorem OAI.Balanced.FieldTransport.mem_mapPoints line 56
  14. theorem OAI.Balanced.FieldTransport.cardinal_field line 60
  15. theorem OAI.Balanced.FieldTransport.direction_fiber_card line 64
  16. theorem OAI.Balanced.FieldTransport.isDeletionSet_transport line 74
  17. theorem OAI.Balanced.FieldTransport.deletionMultiplicity_transport line 84
  18. theorem OAI.Balanced.FieldTransport.uncovered_mem_transport line 92
  19. theorem OAI.Balanced.FieldTransport.uncoveredBy_transport line 104
  20. theorem OAI.Balanced.FieldTransport.linePoints_transport line 110
  21. theorem OAI.Balanced.FieldTransport.lineEquiv_symm line 117
  22. theorem OAI.Balanced.FieldTransport.pointEquiv_symm line 121
  23. theorem OAI.Balanced.FieldTransport.mapLines_symm line 125
  24. def OAI.Balanced.FieldTransport.deletionEquiv line 130
  25. theorem OAI.Balanced.FieldTransport.deletionEquiv_val line 136
  26. theorem OAI.Balanced.FieldTransport.uniformDeletionMass_transport line 139
  27. theorem OAI.Balanced.FieldTransport.empiricalMultiplicityMass_transport line 144
  28. theorem OAI.Balanced.FieldTransport.deletionMultiplicityTV_transport line 155
  29. theorem OAI.Balanced.FieldTransport.mapPoints_inter line 161
  30. theorem OAI.Balanced.FieldTransport.occupancy_card_transport line 164
  31. theorem OAI.Balanced.FieldTransport.exceptionalOccupancyLines_transport line 170
  32. theorem OAI.Balanced.FieldTransport.coversPoints_transport line 180
  33. theorem OAI.Balanced.FieldTransport.disjoint_mapLines line 194
  34. theorem OAI.Balanced.FieldTransport.badCoreCover_map line 198
  35. theorem OAI.Balanced.FieldTransport.badCoreCover_transport line 207
  36. def OAI.Balanced.FieldTransport.mapLaw line 214
  37. theorem OAI.Balanced.FieldTransport.mapLaw_apply line 217
  38. theorem OAI.Balanced.FieldTransport.deletionDominated_transport line 236
  39. theorem OAI.Balanced.FieldTransport.deletionEventProbability_mapLaw line 247
  40. theorem OAI.Balanced.FieldTransport.multiplicity_failure_probability_transport line 257
  41. theorem OAI.Balanced.FieldTransport.occupancy_failure_probability_transport line 264
  42. theorem OAI.Balanced.FieldTransport.core_cover_failure_probability_transport line 274
  43. theorem OAI.Balanced.FieldTransport.same_order_deletion_transport line 281