OAI/Combinatorics/Sensitivity/CompositionFamilies.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The Cartesian block construction works for arbitrary sensitive families.

  1. theorem OAI.Paper320.compose_block_family line 14
  2. theorem OAI.Paper320.compose_block_family_card line 40