OAI/Combinatorics/Sensitivity/RecursiveBlocks.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Disjoint zero-input blocks lift to every column of a chosen row.

  1. def OAI.Paper320.rowLift line 12
  2. theorem OAI.Paper320.mem_rowLift line 19
  3. theorem OAI.Paper320.rowLift_card line 32
  4. theorem OAI.Paper320.rowLift_nonempty line 36
  5. theorem OAI.Paper320.rowLift_disjoint_of_ne line 41
  6. theorem OAI.Paper320.rowLift_disjoint line 47
  7. theorem OAI.Paper320.rowLift_family_disjoint line 54
  8. theorem OAI.Paper320.recursiveChild_rowLift_same line 66
  9. theorem OAI.Paper320.recursiveChild_rowLift_other line 73
  10. theorem OAI.Paper320.recursiveFamily_rowLift line 80