OAI/Combinatorics/BalancedRyser/Probability/UniformConditionalProduct.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.UniformConditionalProduct.subtypeFirstEquiv line 13
  2. def OAI.Balanced.UniformConditionalProduct.conditionedSplitEquiv line 20
  3. theorem OAI.Balanced.UniformConditionalProduct.conditionedSplitEquiv_symm_val line 24
  4. theorem OAI.Balanced.UniformConditionalProduct.uniform_filter_split line 28
  5. theorem OAI.Balanced.UniformConditionalProduct.uniform_map_second line 46
  6. theorem OAI.Balanced.UniformConditionalProduct.uniform_filter_split_second line 54
  7. theorem OAI.Balanced.UniformConditionalProduct.uniform_product_eq_bind line 69
  8. def OAI.Balanced.UniformConditionalProduct.arraySplitEquiv line 81
  9. theorem OAI.Balanced.UniformConditionalProduct.arraySplitEquiv_first line 85
  10. theorem OAI.Balanced.UniformConditionalProduct.arraySplitEquiv_second line 89
  11. theorem OAI.Balanced.UniformConditionalProduct.uniform_filter_array line 93
  12. theorem OAI.Balanced.UniformConditionalProduct.uniform_filter_array_unused line 104