OAI/Computability/PerfectCompleteness/Sampling/CutSamplerReplayGroupingTransport.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CutSamplerReplayGroupingTransport.F2 line 15
  2. theorem OAI.PerfectCompleteness.CutSamplerReplayGroupingTransport.cast_pi_apply line 21
  3. theorem OAI.PerfectCompleteness.CutSamplerReplayGroupingTransport.cast_prod_fst line 29
  4. theorem OAI.PerfectCompleteness.CutSamplerReplayGroupingTransport.cast_prod_snd line 36
  5. theorem OAI.PerfectCompleteness.CutSamplerReplayGroupingTransport.outside_kept line 45
  6. theorem OAI.PerfectCompleteness.CutSamplerReplayGroupingTransport.outside_eq line 66
  7. theorem OAI.PerfectCompleteness.CutSamplerReplayGroupingTransport.retainedChildSlots_eq line 73
  8. theorem OAI.PerfectCompleteness.CutSamplerReplayGroupingTransport.squareEquiv_eq_cast line 83
  9. def OAI.PerfectCompleteness.CutSamplerReplayGroupingTransport.castTerminal line 96
  10. theorem OAI.PerfectCompleteness.CutSamplerReplayGroupingTransport.subExterior_cast line 106
  11. theorem OAI.PerfectCompleteness.CutSamplerReplayGroupingTransport.transport_assemble line 141