OAI/Probability/MatroidProphet/Pivots/Sign.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatroidProphet.Pivots.RealizesSigns line 17
2. def OAI.MatroidProphet.Pivots.affinePatterns line 21
3. lemma OAI.MatroidProphet.Pivots.mem_affinePatterns line 26
4. lemma OAI.MatroidProphet.Pivots.exists_positive_combination line 31
5. lemma OAI.MatroidProphet.Pivots.sum_affine_eq_of_linear_combination_zero line 53
6. lemma OAI.MatroidProphet.Pivots.linearIndependent_of_all_signs line 63
7. lemma OAI.MatroidProphet.Pivots.all_signs_of_shatters line 79
8. lemma OAI.MatroidProphet.Pivots.shatters_card_le_finrank line 96
9. lemma OAI.MatroidProphet.Pivots.card_affinePatterns_le line 104