OAI/Combinatorics/BalancedRyser/Incidence/CandidatePartialPointIncidence.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.CandidatePartialPointIncidence.pmf_probability_mono line 12
2. theorem OAI.Balanced.CandidatePartialPointIncidence.fixedPositions_card_eq_zero_of_card_le_one line 25
3. theorem OAI.Balanced.CandidatePartialPointIncidence.conditional_prescribed_line_probability_le line 33
4. theorem OAI.Balanced.CandidatePartialPointIncidence.conditional_tuple_contains_point_probability_le line 44
5. theorem OAI.Balanced.CandidatePartialPointIncidence.conditional_tuple_through_point_hits_line_probability_le line 60
6. theorem OAI.Balanced.CandidatePartialPointIncidence.conditional_tuple_hits_line_probability_le line 74
7. theorem OAI.Balanced.CandidatePartialPointIncidence.conditional_tuple_hits_two_lines_probability_le line 104