OAI/ModelTheory/Choiceless/Hereditary.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CPTSeparation.Hereditary.mk_out line 13
  2. theorem OAI.CPTSeparation.Hereditary.isSet_mk line 15
  3. theorem OAI.CPTSeparation.Hereditary.isSet_atom line 17
  4. theorem OAI.CPTSeparation.Hereditary.elements_mk line 19
  5. theorem OAI.CPTSeparation.Hereditary.elements_atom line 21
  6. theorem OAI.CPTSeparation.Hereditary.not_mem_atom line 26
  7. theorem OAI.CPTSeparation.Hereditary.atom_injective line 30
  8. theorem OAI.CPTSeparation.Hereditary.isSet_ofFinset line 36
  9. theorem OAI.CPTSeparation.Hereditary.elements_ofFinset line 38
  10. theorem OAI.CPTSeparation.Hereditary.mem_ofFinset line 51
  11. theorem OAI.CPTSeparation.Hereditary.ext_sets line 55
  12. theorem OAI.CPTSeparation.Hereditary.ofFinset_elements line 76
  13. theorem OAI.CPTSeparation.Hereditary.atom_or_set line 82
  14. theorem OAI.CPTSeparation.Hereditary.rank_mk line 90
  15. theorem OAI.CPTSeparation.Hereditary.rank_atom line 92
  16. theorem OAI.CPTSeparation.Hereditary.mem_wellFounded line 94
  17. def OAI.CPTSeparation.Hereditary.rawMap' line 97
  18. def OAI.CPTSeparation.Hereditary.rawMap line 102
  19. theorem OAI.CPTSeparation.Hereditary.toList_rawMap' line 104
  20. theorem OAI.CPTSeparation.Hereditary.rawMap_congr line 111
  21. def OAI.CPTSeparation.Hereditary.map line 123
  22. theorem OAI.CPTSeparation.Hereditary.map_mk line 126
  23. theorem OAI.CPTSeparation.Hereditary.map_atom line 128
  24. theorem OAI.CPTSeparation.Hereditary.isSet_map line 130
  25. theorem OAI.CPTSeparation.Hereditary.elements_map line 134
  26. theorem OAI.CPTSeparation.Hereditary.map_ofFinset line 152
  27. theorem OAI.CPTSeparation.Hereditary.rawMap_id line 160
  28. theorem OAI.CPTSeparation.Hereditary.map_id line 169
  29. theorem OAI.CPTSeparation.Hereditary.rawMap_comp line 175
  30. theorem OAI.CPTSeparation.Hereditary.map_comp line 185
  31. def OAI.CPTSeparation.Hereditary.mapEquiv line 192
  32. instance OAI.CPTSeparation.Hereditary.(instance at line 204) line 204
  33. theorem OAI.CPTSeparation.Hereditary.smul_atom line 217
  34. theorem OAI.CPTSeparation.Hereditary.smul_ofFinset line 220
  35. def OAI.CPTSeparation.Hereditary.Supports line 223
  36. def OAI.CPTSeparation.Hereditary.Supported line 227
  37. def OAI.CPTSeparation.Hereditary.HereditarilySupported line 230
  38. inductive OAI.CPTSeparation.Forms.Form line 243
  39. def OAI.CPTSeparation.Forms.Form.value line 253
  40. theorem OAI.CPTSeparation.Forms.Form.value_atom line 262
  41. theorem OAI.CPTSeparation.Forms.Form.value_set_isSet line 275
  42. theorem OAI.CPTSeparation.Forms.Form.mem_value_set line 289
  43. theorem OAI.CPTSeparation.Forms.Form.value_iso line 308
  44. def OAI.CPTSeparation.Forms.cross31 line 354
  45. def OAI.CPTSeparation.Forms.cross42 line 358
  46. def OAI.CPTSeparation.Forms.cross34 line 362
  47. theorem OAI.CPTSeparation.Forms.swap_type line 366
  48. theorem OAI.CPTSeparation.Forms.elim_comp_cross31 line 378
  49. theorem OAI.CPTSeparation.Forms.elim_comp_cross42 line 382
  50. theorem OAI.CPTSeparation.Forms.elim_comp_cross34 line 386
  51. theorem OAI.CPTSeparation.Forms.set_subset_transfer line 406
  52. theorem OAI.CPTSeparation.Forms.set_eq_forward line 437
  53. theorem OAI.CPTSeparation.Forms.equality_transfer line 460
  54. theorem OAI.CPTSeparation.Forms.membership_forward line 497
  55. theorem OAI.CPTSeparation.Forms.membership_transfer line 521
  56. theorem OAI.CPTSeparation.Forms.value_smul line 544
  57. theorem OAI.CPTSeparation.Forms.value_supported line 563
  58. theorem OAI.CPTSeparation.Forms.hereditary_mem line 584
  59. theorem OAI.CPTSeparation.Forms.hereditary_intro line 598
  60. theorem OAI.CPTSeparation.Forms.value_hereditarily_supported line 614
  61. theorem OAI.CPTSeparation.Forms.smul_mem line 628
  62. theorem OAI.CPTSeparation.Forms.representation line 644
  63. def OAI.CPTSeparation.Counting.triangular line 712
  64. def OAI.CPTSeparation.Counting.snocTuple line 718
  65. theorem OAI.CPTSeparation.Counting.snocTuple_castSucc line 721
  66. theorem OAI.CPTSeparation.Counting.snocTuple_last line 724
  67. def OAI.CPTSeparation.Counting.snocEquiv line 727
  68. def OAI.CPTSeparation.Counting.appendPosition line 735
  69. theorem OAI.CPTSeparation.Counting.tupleType_append_one_bijection line 747
  70. theorem OAI.CPTSeparation.Counting.tupleType_append_fin_bijection line 798
  71. theorem OAI.CPTSeparation.Counting.tupleType_append_bijection line 859
  72. theorem OAI.CPTSeparation.Counting.tupleType_extension_equiv line 881