OAI/Combinatorics/Progressions/Estimates/BSGIndicator.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Set.indicator_one_inter_apply line 27
  2. lemma OAI.Set.indicator_one_inter line 30
  3. lemma OAI.Set.map_indicator_one line 33
  4. lemma OAI.Set.indicator_one_image line 37
  5. lemma OAI.Set.indicator_one_apply_eq_zero line 42
  6. lemma OAI.Set.indicator_one_apply_ne_zero line 45
  7. lemma OAI.Set.indicator_one_eq_zero line 48
  8. lemma OAI.Set.indicator_one_ne_zero line 51
  9. lemma OAI.Set.support_indicator_one line 54
  10. lemma OAI.Set.indicator_one_nonneg line 72
  11. lemma OAI.Set.indicator_one_apply_nonneg line 75
  12. lemma OAI.Set.indicator_one_pos line 84
  13. lemma OAI.Set.conj_indicator_one_apply line 102
  14. lemma OAI.Set.conj_indicator_one line 105