OAI/Combinatorics/HadwigerCounterexample/ConditionalProductLaws.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerCounterexample.subLaw_pair line 13
2. theorem OAI.HadwigerCounterexample.pair_unif line 19
3. theorem OAI.HadwigerCounterexample.unifOn_slice line 23
4. theorem OAI.HadwigerCounterexample.unifOn_and line 47
5. theorem OAI.HadwigerCounterexample.unifOn_and_prod line 68
6. theorem OAI.HadwigerCounterexample.pr_cap line 79
7. def OAI.HadwigerCounterexample.semi line 84
8. theorem OAI.HadwigerCounterexample.semi_avg line 86
9. theorem OAI.HadwigerCounterexample.pair_semi_avg line 90
10. theorem OAI.HadwigerCounterexample.pair_semi_pr line 98
11. theorem OAI.HadwigerCounterexample.prodW_pair_pr line 110

    Source documentation

    Reassociate two arrays of independent columns into componentwise independent pairs.

    theorem prodW_pair_pr (w v : I → Wgt A) (p : I → A × A → Prop) :
        pr (pairW (prodW w) (prodW v)) (fun x => ∀ i, p i (x.1 i,x.2 i)) =
          ∏ i, pr (pairW (w i) (v i)) (p i) := by
    …

    Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.pr, OAI.HadwigerCounterexample.pairW, OAI.HadwigerCounterexample.prodW