OAI/Combinatorics/ListHadwiger/SamplingConnectivity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LinearListHadwiger.Sampling.probability_product_curry line 10
  2. lemma OAI.LinearListHadwiger.Sampling.unionRemainders_survival line 27
  3. theorem OAI.LinearListHadwiger.Sampling.bounded_sampler line 53
  4. theorem OAI.LinearListHadwiger.Sampling.source_private_fractional line 84
  5. lemma OAI.LinearListHadwiger.Knitting.kConnected_image line 175
  6. theorem OAI.LinearListHadwiger.Sampling.complement_failure_on line 216
  7. theorem OAI.LinearListHadwiger.Sampling.source_complement_on line 286