OAI/Combinatorics/BalancedRyser/Profiles/ProfileEmpiricalSupport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.ProfileEmpiricalSupport.empiricalProfileMeasure_compl_eq_zero line 13
2. theorem OAI.Balanced.ProfileEmpiricalSupport.empiricalProfileMeasure_bounded_support line 33
3. theorem OAI.Balanced.ProfileEmpiricalSupport.admissible_empirical_bounded_support line 40
4. theorem OAI.Balanced.ProfileEmpiricalSupport.profileSequenceLimit_bounded line 47
5. theorem OAI.Balanced.ProfileEmpiricalSupport.lineProfile_zero_first_of_mem line 68
6. theorem OAI.Balanced.ProfileEmpiricalSupport.lineProfile_zero_second_of_mem line 82
7. theorem OAI.Balanced.ProfileEmpiricalSupport.profileSequenceLimit_zero_coordinates line 96