OAI/Combinatorics/ParityLifts/BaseLabels.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ParityWL.baseType_inl_iff line 15
  2. lemma OAI.ParityWL.baseType_inr_iff line 29
  3. lemma OAI.ParityWL.base_main_label line 43
  4. lemma OAI.ParityWL.base_helper_left_label line 77
  5. lemma OAI.ParityWL.base_helper_right_label line 108
  6. def OAI.ParityWL.leftLabelAt line 139
  7. def OAI.ParityWL.rightLabelAt line 143
  8. def OAI.ParityWL.helperLabelAt line 147
  9. lemma OAI.ParityWL.leftLabelAt_self line 151
  10. lemma OAI.ParityWL.rightLabelAt_self line 155
  11. lemma OAI.ParityWL.helperLabelAt_self line 159
  12. lemma OAI.ParityWL.base_main_labels line 163
  13. lemma OAI.ParityWL.base_helper_left_labels line 170
  14. lemma OAI.ParityWL.base_helper_right_labels line 178