OAI/Combinatorics/BalancedRyser/Incidence/CandidateFreshIncidence.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.CandidateFreshIncidence.positionProbability line 13
  2. theorem OAI.Balanced.CandidateFreshIncidence.offset_probability_eq line 16
  3. theorem OAI.Balanced.CandidateFreshIncidence.positionProbability_eq_card line 26
  4. theorem OAI.Balanced.CandidateFreshIncidence.positionProbability_mono line 38
  5. theorem OAI.Balanced.CandidateFreshIncidence.positionProbability_exists_le line 46
  6. theorem OAI.Balanced.CandidateFreshIncidence.positionProbability_rectangle line 69
  7. theorem OAI.Balanced.CandidateFreshIncidence.positionProbability_one_fixed line 84
  8. theorem OAI.Balanced.CandidateFreshIncidence.aligned_fixed_position_le line 94
  9. theorem OAI.Balanced.CandidateFreshIncidence.same_direction_fixed_position_le line 105
  10. theorem OAI.Balanced.CandidateFreshIncidence.aligned_probability line 118
  11. theorem OAI.Balanced.CandidateFreshIncidence.positionProbability_exists_le_card line 132
  12. theorem OAI.Balanced.CandidateFreshIncidence.same_direction_position_on_line_le line 142
  13. theorem OAI.Balanced.CandidateFreshIncidence.same_direction_hits_line_le line 172
  14. theorem OAI.Balanced.CandidateFreshIncidence.same_direction_contains_point_le line 185
  15. theorem OAI.Balanced.CandidateFreshIncidence.aligned_position_on_other_line_le line 198
  16. theorem OAI.Balanced.CandidateFreshIncidence.through_point_hits_line_le line 213
  17. theorem OAI.Balanced.CandidateFreshIncidence.positionProbability_two_fixed line 231
  18. theorem OAI.Balanced.CandidateFreshIncidence.aligned_two_fixed_le line 242
  19. theorem OAI.Balanced.CandidateFreshIncidence.same_direction_two_positions_lines_le line 257
  20. theorem OAI.Balanced.CandidateFreshIncidence.same_direction_hits_two_lines_le line 303
  21. theorem OAI.Balanced.CandidateFreshIncidence.tuple_hits_line_probability_le line 321
  22. theorem OAI.Balanced.CandidateFreshIncidence.tuple_contains_point_probability_le line 331
  23. theorem OAI.Balanced.CandidateFreshIncidence.tuple_through_point_hits_line_probability_le line 341
  24. theorem OAI.Balanced.CandidateFreshIncidence.tuple_hits_two_lines_probability_le line 352