OAI/Combinatorics/ParityLifts/ChoiceExtraction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ParityWL.mismatch_side_zero line 17
2. lemma OAI.ParityWL.BalancedStar.partition_testMass line 59
3. theorem OAI.ParityWL.choice_of_balancedStar line 68

   Source documentation

   The helper boundary argument from a finite partition around a balanced bag.

   theorem choice_of_balancedStar (s : BalancedStar w) (ht : 0 < t) : C.Successful := by
   …

   Mentions: OAI.ParityWL.BalancedStar