OAI/Computability/DirectedFeedback/Games/DegreeCover.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Appendix.DegreeCover.F2 line 8
  2. theorem OAI.DFVSGames.Appendix.DegreeCover.binary_add_self line 12
  3. theorem OAI.DFVSGames.Appendix.DegreeCover.binary_neg line 16
  4. theorem OAI.DFVSGames.Appendix.DegreeCover.exists_glue_zero line 20
  5. theorem OAI.DFVSGames.Appendix.DegreeCover.binary_cross_inline_DegreeCover line 42
  6. theorem OAI.DFVSGames.Appendix.DegreeCover.exists_cover_component line 50
  7. theorem OAI.DFVSGames.Appendix.DegreeCover.exists_disjoint_decomposition line 88
  8. theorem OAI.DFVSGames.Appendix.DegreeCover.rank_add_of_disjoint line 150
  9. theorem OAI.DFVSGames.Appendix.DegreeCover.outside_bad_rank_cover line 163
  10. abbrev OAI.DFVSGames.Appendix.Identities.Vector line 191
  11. def OAI.DFVSGames.Appendix.Identities.add line 193
  12. def OAI.DFVSGames.Appendix.Identities.zero line 195
  13. theorem OAI.DFVSGames.Appendix.Identities.add_assoc line 197
  14. theorem OAI.DFVSGames.Appendix.Identities.add_self line 202
  15. theorem OAI.DFVSGames.Appendix.Identities.add_zero line 206
  16. theorem OAI.DFVSGames.Appendix.Identities.zero_add line 210
  17. theorem OAI.DFVSGames.Appendix.Identities.add_comm line 214
  18. theorem OAI.DFVSGames.Appendix.Identities.add_shuffle line 218
  19. structure OAI.DFVSGames.Appendix.Identities.Subspace line 224
  20. def OAI.DFVSGames.Appendix.Identities.Subspace.Included line 229
  21. structure OAI.DFVSGames.Appendix.Identities.LinearMap line 232
  22. def OAI.DFVSGames.Appendix.Identities.Hybrid line 237
  23. def OAI.DFVSGames.Appendix.Identities.OuterHybrid line 242
  24. theorem OAI.DFVSGames.Appendix.Identities.nested_hybrid_selector_iff line 248
  25. def OAI.DFVSGames.Appendix.Identities.ImagesDisjointModulo line 285
  26. theorem OAI.DFVSGames.Appendix.Identities.reverse_sum_image line 290
  27. theorem OAI.DFVSGames.Appendix.Identities.reverse_sum_preimage line 306
  28. def OAI.DFVSGames.Appendix.LinearIdentities.Hybrid line 334
  29. def OAI.DFVSGames.Appendix.LinearIdentities.compress line 337
  30. theorem OAI.DFVSGames.Appendix.LinearIdentities.compress_apply line 340
  31. theorem OAI.DFVSGames.Appendix.LinearIdentities.compress_sub line 343
  32. theorem OAI.DFVSGames.Appendix.LinearIdentities.quotient_mem_image_iff line 348
  33. theorem OAI.DFVSGames.Appendix.LinearIdentities.nested_hybrid_iff line 353
  34. theorem OAI.DFVSGames.Appendix.LinearIdentities.compress_rank_preserved line 404
  35. theorem OAI.DFVSGames.Appendix.LinearIdentities.reverse_hybrid_of_compressed_rankBelow line 428
  36. theorem OAI.DFVSGames.Appendix.LinearIdentities.rankBelow_of_compressed_rankBelow line 473
  37. theorem OAI.DFVSGames.Appendix.LinearIdentities.image_inter_complement_eq line 499
  38. theorem OAI.DFVSGames.Appendix.LinearIdentities.domain_complement_eq line 516
  39. theorem OAI.DFVSGames.Appendix.LinearIdentities.surviving_pair_forced line 530
  40. theorem OAI.DFVSGames.Appendix.LinearIdentities.canonical_inner_hybrid line 558
  41. theorem OAI.DFVSGames.Appendix.LinearIdentities.canonical_remainder_hybrid line 581
  42. theorem OAI.DFVSGames.Appendix.LinearIdentities.canonical_codomain_complement line 611
  43. theorem OAI.DFVSGames.Appendix.LinearIdentities.canonical_domain_complement line 637
  44. theorem OAI.DFVSGames.Appendix.LinearIdentities.compressed_rankBelow_of_hybrids line 673
  45. theorem OAI.DFVSGames.Appendix.LinearIdentities.reverse_outer_hybrid line 696
  46. def OAI.DFVSGames.Appendix.LinearIdentities.A5PairSurvives line 742
  47. theorem OAI.DFVSGames.Appendix.LinearIdentities.a5_unique_selector line 750
  48. theorem OAI.DFVSGames.Appendix.LinearIdentities.a4_codomain_forced line 777
  49. theorem OAI.DFVSGames.Appendix.LinearIdentities.a4_domain_forced line 815
  50. theorem OAI.DFVSGames.Appendix.LinearIdentities.a4_apply_on_preimage line 857
  51. theorem OAI.DFVSGames.Appendix.LinearIdentities.a4_map_unique line 875
  52. theorem OAI.DFVSGames.Appendix.LinearIdentities.a4_weak_selector_of_summand line 904
  53. theorem OAI.DFVSGames.Appendix.LinearIdentities.a4_kernel_of_gluing line 933
  54. theorem OAI.DFVSGames.Appendix.LinearIdentities.disjoint_quotient_images_of_intersection line 974
  55. theorem OAI.DFVSGames.Appendix.LinearIdentities.a4_range_of_gluing line 994
  56. theorem OAI.DFVSGames.Appendix.LinearIdentities.a4_remainder_of_gluing line 1021
  57. abbrev OAI.DFVSGames.Appendix.LinearIdentities.A4Index line 1054
  58. def OAI.DFVSGames.Appendix.LinearIdentities.A4Survives line 1056
  59. theorem OAI.DFVSGames.Appendix.LinearIdentities.a4_surviving_index_unique line 1064
  60. abbrev OAI.DFVSGames.Appendix.BinaryA4.F2 line 1088
  61. theorem OAI.DFVSGames.Appendix.BinaryA4.canonical_glued_map line 1094
  62. theorem OAI.DFVSGames.Appendix.BinaryA4.a4_selector_exists line 1128
  63. theorem OAI.DFVSGames.Appendix.BinaryA4.a4_unique_selector line 1153