OAI/Probability/ClassicalON/ProductGrouping.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ClassicalON.GroupedFamily line 14
2. def OAI.ClassicalON.groupedEquiv line 16
3. def OAI.ClassicalON.groupedMeasurableEquiv line 28
4. theorem OAI.ClassicalON.grouped_measurePreserving line 33
5. theorem OAI.ClassicalON.integral_grouped_product line 58
6. theorem OAI.ClassicalON.sum_grouped_product line 75