OAI/Probability/SignedSweeps/BlockRestriction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.blockFiberEquiv line 10
  2. lemma OAI.SignedSweeps.blockFiberEquiv_apply line 25
  3. lemma OAI.SignedSweeps.blockPermutation_exists line 29
  4. lemma OAI.SignedSweeps.blockPermutation_range line 46
  5. def OAI.SignedSweeps.BlockInjectionSquare line 53
  6. lemma OAI.SignedSweeps.blockInjection_route line 59
  7. lemma OAI.SignedSweeps.blockInjection_range line 68
  8. lemma OAI.SignedSweeps.viaEmbedding_blockPermutation line 84
  9. theorem OAI.SignedSweeps.block_coefficient_restriction line 102