OAI/Combinatorics/SumProduct/Alignment/Blocks02.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceBlocks.targetBlock line 48
  2. lemma OAI.SourceBlocks.targetBlock_target line 50
  3. lemma OAI.SourceBlocks.targetBlock_set line 53
  4. lemma OAI.SourceBlocks.targetBlock_block line 56
  5. lemma OAI.SourceBlocks.pair_injective line 61
  6. def OAI.SourceBlocks.subsetPairs line 68
  7. lemma OAI.SourceBlocks.mem_subsetPairs line 73
  8. lemma OAI.SourceBlocks.subsetPairs_sum line 78
  9. abbrev OAI.SourceBlocks.Models line 94
  10. def OAI.SourceBlocks.scalar line 98
  11. lemma OAI.SourceBlocks.scalar_canonical line 102
  12. def OAI.SourceBlocks.offset line 110
  13. def OAI.SourceBlocks.aligned line 118
  14. theorem OAI.SourceBlocks.aligned_of_canonical line 128
  15. structure OAI.SourceFiniteMenuModels.System line 174
  16. def OAI.SourceFiniteMenuModels.extended line 186
  17. lemma OAI.SourceFiniteMenuModels.extended_eq line 189
  18. def OAI.SourceFiniteMenuModels.charted line 194
  19. lemma OAI.SourceFiniteMenuModels.charted_models line 237
  20. theorem OAI.SourceFiniteMenuModels.represents_all line 260
  21. instance OAI.SourceMenuAlignment.law_probability line 284
  22. def OAI.SourceMenuAlignment.tuples line 289
  23. def OAI.SourceMenuAlignment.values line 292
  24. lemma OAI.SourceMenuAlignment.closure line 295
  25. lemma OAI.SourceMenuAlignment.tuples_pos line 299
  26. lemma OAI.SourceMenuAlignment.values_pos line 303
  27. def OAI.SourceMenuAlignment.event line 312
  28. theorem OAI.SourceMenuAlignment.menu_alignment_eventually line 318
  29. theorem OAI.SourceMenuAlignment.menu_alignment_liminf line 340