OAI/Combinatorics/HadwigerCounterexample/ProductLaws.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerCounterexample.ind_all line 13
2. def OAI.HadwigerCounterexample.prodW line 21
3. theorem OAI.HadwigerCounterexample.prodW_tot line 26
4. theorem OAI.HadwigerCounterexample.prodW_avg line 29
5. theorem OAI.HadwigerCounterexample.prodW_pr line 35
6. theorem OAI.HadwigerCounterexample.prodW_nonneg line 41
7. theorem OAI.HadwigerCounterexample.prodW_law line 44
8. theorem OAI.HadwigerCounterexample.prodW_pr_inj line 55

   Source documentation

   Observe distinct coordinates of a (constant-type) product law.

   theorem prodW_pr_inj {e : ι → κ} (he : Function.Injective e)
       {w : κ → Wgt α} (hw : ∀ k, IsLaw (w k)) (p : ι → α → Prop) :
       pr (prodW (β:=fun _ => α) w) (fun x => ∀ i, p i (x (e i))) =
   …

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

9. theorem OAI.HadwigerCounterexample.prodW_map_inj line 86
10. theorem OAI.HadwigerCounterexample.prodW_map_pairs line 98

    Source documentation

    Mapping to ordered pairs along a disjoint family of positions.

    theorem prodW_map_pairs (e : ι ⊕ ι → κ) (he : Function.Injective e)
        {w : Wgt α} (hw : IsLaw w) :
        mapW (prodW (fun _ : κ => w))
          (fun x i => (x (e (.inl i)), x (e (.inr i)))) =
          prodW (fun _ : ι => pairW w w) := by
    …

    Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.IsLaw, OAI.HadwigerCounterexample.mapW, OAI.HadwigerCounterexample.prodW, OAI.HadwigerCounterexample.pairW